YES 7.589 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule FiniteMap
  ((lookupFM :: (Ord a, Ord b) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c) :: (Ord a, Ord b) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm foldFM (\key elt rest ->(key,elt: rest) [] fm

  foldFM :: (c  ->  b  ->  a  ->  a ->  a  ->  FiniteMap c b  ->  a
foldFM k z EmptyFM z
foldFM k z (Branch key elt _ fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key Nothing
lookupFM (Branch key elt _ fm_l fm_rkey_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch _ _ size _ _) size


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\keyeltrest→(key,elt: rest

is transformed to
fmToList0 key elt rest = (key,elt: rest



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule FiniteMap
  ((lookupFM :: (Ord c, Ord b) => FiniteMap (b,c) a  ->  (b,c ->  Maybe a) :: (Ord c, Ord b) => FiniteMap (b,c) a  ->  (b,c ->  Maybe a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (a  ->  c  ->  b  ->  b ->  b  ->  FiniteMap a c  ->  b
foldFM k z EmptyFM z
foldFM k z (Branch key elt _ fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key Nothing
lookupFM (Branch key elt _ fm_l fm_rkey_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch _ _ size _ _) size


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Case Reductions:
The following Case expression
case compare x y of
 EQ → o
 LT → LT
 GT → GT

is transformed to
primCompAux0 o EQ = o
primCompAux0 o LT = LT
primCompAux0 o GT = GT



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule FiniteMap
  ((lookupFM :: (Ord b, Ord a) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c) :: (Ord b, Ord a) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap b a  ->  [(b,a)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (b  ->  c  ->  a  ->  a ->  a  ->  FiniteMap b c  ->  a
foldFM k z EmptyFM z
foldFM k z (Branch key elt _ fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key Nothing
lookupFM (Branch key elt _ fm_l fm_rkey_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch _ _ size _ _) size


module Maybe where
  import qualified FiniteMap
import qualified Prelude



If Reductions:
The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule FiniteMap
  ((lookupFM :: (Ord b, Ord a) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c) :: (Ord b, Ord a) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap b a  ->  [(b,a)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (c  ->  a  ->  b  ->  b ->  b  ->  FiniteMap c a  ->  b
foldFM k z EmptyFM z
foldFM k z (Branch key elt _ fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key Nothing
lookupFM (Branch key elt _ fm_l fm_rkey_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch _ _ size _ _) size


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule FiniteMap
  ((lookupFM :: (Ord a, Ord b) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c) :: (Ord b, Ord a) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (a  ->  c  ->  b  ->  b ->  b  ->  FiniteMap a c  ->  b
foldFM k z EmptyFM z
foldFM k z (Branch key elt vw fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key Nothing
lookupFM (Branch key elt vx fm_l fm_rkey_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch vy vz size wu wvsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Cond Reductions:
The following Function with conditions
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt vx fm_l fm_rkey_to_find
 | key_to_find < key
 = lookupFM fm_l key_to_find
 | key_to_find > key
 = lookupFM fm_r key_to_find
 | otherwise
 = Just elt

is transformed to
lookupFM EmptyFM key = lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_rkey_to_find = lookupFM3 (Branch key elt vx fm_l fm_rkey_to_find

lookupFM2 key elt vx fm_l fm_r key_to_find True = lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False = lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

lookupFM0 key elt vx fm_l fm_r key_to_find True = Just elt

lookupFM1 key elt vx fm_l fm_r key_to_find True = lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False = lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

lookupFM3 (Branch key elt vx fm_l fm_rkey_to_find = lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

lookupFM4 EmptyFM key = Nothing
lookupFM4 vvu vvv = lookupFM3 vvu vvv

The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare0 x y True = GT

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare3 x y = compare2 x y (x == y)

The following Function with conditions
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd' x vvw = gcd'2 x vvw
gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vvw = x
gcd'1 vvx vvy vvz = gcd'0 vvy vvz

gcd'2 x vvw = gcd'1 (vvw == 0) x vvw
gcd'2 vwu vwv = gcd'0 vwu vwv

The following Function with conditions
gcd 0 0 = error []
gcd x y = 
gcd' (abs x) (abs y)
where 
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd vww vwx = gcd3 vww vwx
gcd x y = gcd0 x y

gcd0 x y = 
gcd' (abs x) (abs y)
where 
gcd' x vvw = gcd'2 x vvw
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vvw = x
gcd'1 vvx vvy vvz = gcd'0 vvy vvz
gcd'2 x vvw = gcd'1 (vvw == 0) x vvw
gcd'2 vwu vwv = gcd'0 vwu vwv

gcd1 True vww vwx = error []
gcd1 vwy vwz vxu = gcd0 vwz vxu

gcd2 True vww vwx = gcd1 (vwx == 0) vww vwx
gcd2 vxv vxw vxx = gcd0 vxw vxx

gcd3 vww vwx = gcd2 (vww == 0) vww vwx
gcd3 vxy vxz = gcd0 vxy vxz

The following Function with conditions
absReal x
 | x >= 0
 = x
 | otherwise
 = `negate` x

is transformed to
absReal x = absReal2 x

absReal0 x True = `negate` x

absReal1 x True = x
absReal1 x False = absReal0 x otherwise

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
reduce x y
 | y == 0
 = error []
 | otherwise
 = x `quot` d :% (y `quot` d)
where 
d  = gcd x y

is transformed to
reduce x y = reduce2 x y

reduce2 x y = 
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ LetRed

mainModule FiniteMap
  ((lookupFM :: (Ord a, Ord b) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c) :: (Ord b, Ord a) => FiniteMap (b,a) c  ->  (b,a ->  Maybe c)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (b  ->  c  ->  a  ->  a ->  a  ->  FiniteMap b c  ->  a
foldFM k z EmptyFM z
foldFM k z (Branch key elt vw fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_rkey_to_find lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

  
lookupFM0 key elt vx fm_l fm_r key_to_find True Just elt

  
lookupFM1 key elt vx fm_l fm_r key_to_find True lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

  
lookupFM2 key elt vx fm_l fm_r key_to_find True lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

  
lookupFM3 (Branch key elt vx fm_l fm_rkey_to_find lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

  
lookupFM4 EmptyFM key Nothing
lookupFM4 vvu vvv lookupFM3 vvu vvv

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch vy vz size wu wvsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level
reduce2D vyu vyv = gcd vyu vyv

reduce2Reduce0 vyu vyv x y True = x `quot` reduce2D vyu vyv :% (y `quot` reduce2D vyu vyv)

reduce2Reduce1 vyu vyv x y True = error []
reduce2Reduce1 vyu vyv x y False = reduce2Reduce0 vyu vyv x y otherwise

The bindings of the following Let/Where expression
gcd' (abs x) (abs y)
where 
gcd' x vvw = gcd'2 x vvw
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vvw = x
gcd'1 vvx vvy vvz = gcd'0 vvy vvz
gcd'2 x vvw = gcd'1 (vvw == 0) x vvw
gcd'2 vwu vwv = gcd'0 vwu vwv

are unpacked to the following functions on top level
gcd0Gcd' x vvw = gcd0Gcd'2 x vvw
gcd0Gcd' x y = gcd0Gcd'0 x y

gcd0Gcd'2 x vvw = gcd0Gcd'1 (vvw == 0) x vvw
gcd0Gcd'2 vwu vwv = gcd0Gcd'0 vwu vwv

gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd'1 True x vvw = x
gcd0Gcd'1 vvx vvy vvz = gcd0Gcd'0 vvy vvz



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
HASKELL
                          ↳ NumRed

mainModule FiniteMap
  ((lookupFM :: (Ord a, Ord c) => FiniteMap (a,c) b  ->  (a,c ->  Maybe b) :: (Ord c, Ord a) => FiniteMap (a,c) b  ->  (a,c ->  Maybe b)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (a  ->  c  ->  b  ->  b ->  b  ->  FiniteMap a c  ->  b
foldFM k z EmptyFM z
foldFM k z (Branch key elt vw fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_rkey_to_find lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

  
lookupFM0 key elt vx fm_l fm_r key_to_find True Just elt

  
lookupFM1 key elt vx fm_l fm_r key_to_find True lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

  
lookupFM2 key elt vx fm_l fm_r key_to_find True lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

  
lookupFM3 (Branch key elt vx fm_l fm_rkey_to_find lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

  
lookupFM4 EmptyFM key Nothing
lookupFM4 vvu vvv lookupFM3 vvu vvv

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch vy vz size wu wvsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
HASKELL
                              ↳ Narrow

mainModule FiniteMap
  (lookupFM :: (Ord b, Ord a) => FiniteMap (a,b) c  ->  (a,b ->  Maybe c)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  fmToList :: FiniteMap b a  ->  [(b,a)]
fmToList fm foldFM fmToList0 [] fm

  
fmToList0 key elt rest (key,elt: rest

  foldFM :: (b  ->  c  ->  a  ->  a ->  a  ->  FiniteMap b c  ->  a
foldFM k z EmptyFM z
foldFM k z (Branch key elt vw fm_l fm_rfoldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_rkey_to_find lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

  
lookupFM0 key elt vx fm_l fm_r key_to_find True Just elt

  
lookupFM1 key elt vx fm_l fm_r key_to_find True lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

  
lookupFM2 key elt vx fm_l fm_r key_to_find True lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

  
lookupFM3 (Branch key elt vx fm_l fm_rkey_to_find lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

  
lookupFM4 EmptyFM key Nothing
lookupFM4 vvu vvv lookupFM3 vvu vvv

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM Pos Zero
sizeFM (Branch vy vz size wu wvsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(vyw4000), Succ(vyw30000)) → new_primEqNat(vyw4000, vyw30000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vyw7900), Succ(vyw3000000)) → new_primPlusNat(vyw7900, vyw3000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vyw40000), Succ(vyw300000)) → new_primMulNat(vyw40000, Succ(vyw300000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vyw43000), Succ(vyw45000)) → new_primCmpNat(vyw43000, vyw45000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), bae, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs1(vyw401, vyw3001, bba, bbb, bbc)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, app(app(ty_@2, ha), hb), gc) → new_esEs2(vyw401, vyw3001, ha, hb)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, app(ty_Maybe, gb), gc) → new_esEs(vyw401, vyw3001, gb)
new_esEs0(Right(vyw400), Right(vyw3000), dd, app(app(ty_@2, ec), ed)) → new_esEs2(vyw400, vyw3000, ec, ed)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, app(app(app(ty_@3, gf), gg), gh), gc) → new_esEs1(vyw401, vyw3001, gf, gg, gh)
new_esEs3(:(vyw400, vyw401), :(vyw3000, vyw3001), app(ty_[], beb)) → new_esEs3(vyw400, vyw3000, beb)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), bae, app(app(ty_@2, bbd), bbe)) → new_esEs2(vyw401, vyw3001, bbd, bbe)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), bae, app(ty_Maybe, baf)) → new_esEs(vyw401, vyw3001, baf)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, eg, app(ty_[], ga)) → new_esEs3(vyw402, vyw3002, ga)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), app(ty_Maybe, bbg), bbh) → new_esEs(vyw400, vyw3000, bbg)
new_esEs(Just(vyw400), Just(vyw3000), app(ty_[], bh)) → new_esEs3(vyw400, vyw3000, bh)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, eg, app(app(app(ty_@3, fc), fd), ff)) → new_esEs1(vyw402, vyw3002, fc, fd, ff)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), app(app(ty_@2, bcf), bcg), bbh) → new_esEs2(vyw400, vyw3000, bcf, bcg)
new_esEs(Just(vyw400), Just(vyw3000), app(ty_Maybe, h)) → new_esEs(vyw400, vyw3000, h)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), bae, app(app(ty_Either, bag), bah)) → new_esEs0(vyw401, vyw3001, bag, bah)
new_esEs0(Left(vyw400), Left(vyw3000), app(app(ty_Either, cc), cd), cb) → new_esEs0(vyw400, vyw3000, cc, cd)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), app(app(app(ty_@3, bcc), bcd), bce), bbh) → new_esEs1(vyw400, vyw3000, bcc, bcd, bce)
new_esEs0(Left(vyw400), Left(vyw3000), app(app(ty_@2, da), db), cb) → new_esEs2(vyw400, vyw3000, da, db)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), app(ty_[], bad), eg, gc) → new_esEs3(vyw400, vyw3000, bad)
new_esEs3(:(vyw400, vyw401), :(vyw3000, vyw3001), bda) → new_esEs3(vyw401, vyw3001, bda)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), app(ty_Maybe, hd), eg, gc) → new_esEs(vyw400, vyw3000, hd)
new_esEs0(Right(vyw400), Right(vyw3000), dd, app(app(ty_Either, df), dg)) → new_esEs0(vyw400, vyw3000, df, dg)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, eg, app(app(ty_@2, fg), fh)) → new_esEs2(vyw402, vyw3002, fg, fh)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, app(ty_[], hc), gc) → new_esEs3(vyw401, vyw3001, hc)
new_esEs(Just(vyw400), Just(vyw3000), app(app(ty_Either, ba), bb)) → new_esEs0(vyw400, vyw3000, ba, bb)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), app(app(app(ty_@3, hg), hh), baa), eg, gc) → new_esEs1(vyw400, vyw3000, hg, hh, baa)
new_esEs(Just(vyw400), Just(vyw3000), app(app(ty_@2, bf), bg)) → new_esEs2(vyw400, vyw3000, bf, bg)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), app(app(ty_Either, he), hf), eg, gc) → new_esEs0(vyw400, vyw3000, he, hf)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, app(app(ty_Either, gd), ge), gc) → new_esEs0(vyw401, vyw3001, gd, ge)
new_esEs0(Left(vyw400), Left(vyw3000), app(ty_[], dc), cb) → new_esEs3(vyw400, vyw3000, dc)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, eg, app(app(ty_Either, fa), fb)) → new_esEs0(vyw402, vyw3002, fa, fb)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), app(ty_[], bch), bbh) → new_esEs3(vyw400, vyw3000, bch)
new_esEs0(Right(vyw400), Right(vyw3000), dd, app(ty_Maybe, de)) → new_esEs(vyw400, vyw3000, de)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), bae, app(ty_[], bbf)) → new_esEs3(vyw401, vyw3001, bbf)
new_esEs2(@2(vyw400, vyw401), @2(vyw3000, vyw3001), app(app(ty_Either, bca), bcb), bbh) → new_esEs0(vyw400, vyw3000, bca, bcb)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), app(app(ty_@2, bab), bac), eg, gc) → new_esEs2(vyw400, vyw3000, bab, bac)
new_esEs3(:(vyw400, vyw401), :(vyw3000, vyw3001), app(app(ty_@2, bdh), bea)) → new_esEs2(vyw400, vyw3000, bdh, bea)
new_esEs3(:(vyw400, vyw401), :(vyw3000, vyw3001), app(app(ty_Either, bdc), bdd)) → new_esEs0(vyw400, vyw3000, bdc, bdd)
new_esEs(Just(vyw400), Just(vyw3000), app(app(app(ty_@3, bc), bd), be)) → new_esEs1(vyw400, vyw3000, bc, bd, be)
new_esEs0(Left(vyw400), Left(vyw3000), app(ty_Maybe, ca), cb) → new_esEs(vyw400, vyw3000, ca)
new_esEs3(:(vyw400, vyw401), :(vyw3000, vyw3001), app(ty_Maybe, bdb)) → new_esEs(vyw400, vyw3000, bdb)
new_esEs3(:(vyw400, vyw401), :(vyw3000, vyw3001), app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs1(vyw400, vyw3000, bde, bdf, bdg)
new_esEs0(Right(vyw400), Right(vyw3000), dd, app(ty_[], ee)) → new_esEs3(vyw400, vyw3000, ee)
new_esEs0(Left(vyw400), Left(vyw3000), app(app(app(ty_@3, ce), cf), cg), cb) → new_esEs1(vyw400, vyw3000, ce, cf, cg)
new_esEs1(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ef, eg, app(ty_Maybe, eh)) → new_esEs(vyw402, vyw3002, eh)
new_esEs0(Right(vyw400), Right(vyw3000), dd, app(app(app(ty_@3, dh), ea), eb)) → new_esEs1(vyw400, vyw3000, dh, ea, eb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_ltEs3(Left(vyw4310), Left(vyw4510), app(app(ty_Either, bdc), bdd), bce) → new_ltEs3(vyw4310, vyw4510, bdc, bdd)
new_lt(vyw430, vyw450, bag, bah) → new_compare20(vyw430, vyw450, new_esEs4(vyw430, vyw450, bag, bah), bag, bah)
new_compare2(vyw430, vyw450, beh, bfa, bfb) → new_compare21(vyw430, vyw450, new_esEs5(vyw430, vyw450, beh, bfa, bfb), beh, bfa, bfb)
new_compare20(@2(:(vyw4300, vyw4301), vyw431), @2(:(vyw4500, vyw4501), vyw451), False, app(ty_[], he), beg) → new_primCompAux(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, he), he)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), h, app(ty_Maybe, bg)) → new_ltEs2(vyw4311, vyw4511, bg)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, h), app(app(ty_@2, ba), bb))) → new_ltEs(vyw4311, vyw4511, ba, bb)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, app(ty_[], gh)), df), fb)) → new_lt1(vyw4310, vyw4510, gh)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, df, app(app(ty_@2, dg), dh)) → new_ltEs(vyw4312, vyw4512, dg, dh)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, app(app(ty_Either, dc), dd)), cd)) → new_lt3(vyw4310, vyw4510, dc, dd)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), df), app(ty_[], ed))) → new_ltEs1(vyw4312, vyw4512, ed)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(ty_Maybe, ha), df, fb) → new_lt2(vyw4310, vyw4510, ha)
new_lt1(:(vyw4300, vyw4301), :(vyw4500, vyw4501), he) → new_primCompAux(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, he), he)
new_compare20(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bba, app(ty_Maybe, app(app(app(ty_@3, bbd), bbe), bbf))) → new_ltEs0(vyw4310, vyw4510, bbd, bbe, bbf)
new_ltEs3(Right(vyw4310), Right(vyw4510), bde, app(app(app(ty_@3, bdh), bea), beb)) → new_ltEs0(vyw4310, vyw4510, bdh, bea, beb)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, h), app(app(ty_Either, bh), ca))) → new_ltEs3(vyw4311, vyw4511, bh, ca)
new_compare20(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bba, app(app(ty_Either, app(app(ty_@2, bcc), bcd)), bce)) → new_ltEs(vyw4310, vyw4510, bcc, bcd)
new_primCompAux(vyw4300, vyw4500, vyw107, app(ty_[], bac)) → new_compare(vyw4300, vyw4500, bac)
new_compare20(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(ty_Maybe, bfc), beg) → new_compare22(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfc), bfc)
new_compare20(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bba, app(app(ty_Either, bde), app(ty_[], bec))) → new_ltEs1(vyw4310, vyw4510, bec)
new_ltEs2(Just(vyw4310), Just(vyw4510), app(app(app(ty_@3, bbd), bbe), bbf)) → new_ltEs0(vyw4310, vyw4510, bbd, bbe, bbf)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), app(app(app(ty_@3, fc), fd), ff)), fb)) → new_lt0(vyw4311, vyw4511, fc, fd, ff)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, app(app(ty_@2, gc), gd)), df), fb)) → new_lt(vyw4310, vyw4510, gc, gd)
new_lt1(:(vyw4300, vyw4301), :(vyw4500, vyw4501), he) → new_compare(vyw4301, vyw4501, he)
new_ltEs3(Right(vyw4310), Right(vyw4510), bde, app(app(ty_Either, bee), bef)) → new_ltEs3(vyw4310, vyw4510, bee, bef)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, app(app(ty_@2, cb), cc)), cd)) → new_lt(vyw4310, vyw4510, cb, cc)
new_compare20(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(app(app(ty_@3, beh), bfa), bfb), beg) → new_compare21(vyw430, vyw450, new_esEs5(vyw430, vyw450, beh, bfa, bfb), beh, bfa, bfb)
new_lt0(vyw430, vyw450, beh, bfa, bfb) → new_compare21(vyw430, vyw450, new_esEs5(vyw430, vyw450, beh, bfa, bfb), beh, bfa, bfb)
new_ltEs2(Just(vyw4310), Just(vyw4510), app(ty_[], bbg)) → new_ltEs1(vyw4310, vyw4510, bbg)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), app(ty_Maybe, fh)), fb)) → new_lt2(vyw4311, vyw4511, fh)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, app(app(ty_Either, hb), hc)), df), fb)) → new_lt3(vyw4310, vyw4510, hb, hc)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(ty_[], gh), df, fb) → new_lt1(vyw4310, vyw4510, gh)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, df, app(app(app(ty_@3, ea), eb), ec)) → new_ltEs0(vyw4312, vyw4512, ea, eb, ec)
new_compare23(vyw430, vyw450, False, bfd, bfe) → new_ltEs3(vyw430, vyw450, bfd, bfe)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, app(app(ty_@2, eh), fa), fb) → new_lt(vyw4311, vyw4511, eh, fa)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, df, app(ty_[], ed)) → new_ltEs1(vyw4312, vyw4512, ed)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), df), app(app(ty_Either, ef), eg))) → new_ltEs3(vyw4312, vyw4512, ef, eg)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), df), app(app(ty_@2, dg), dh))) → new_ltEs(vyw4312, vyw4512, dg, dh)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), h, app(app(ty_Either, bh), ca)) → new_ltEs3(vyw4311, vyw4511, bh, ca)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), h, app(app(ty_@2, ba), bb)) → new_ltEs(vyw4311, vyw4511, ba, bb)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(app(ty_Either, dc), dd), cd) → new_lt3(vyw4310, vyw4510, dc, dd)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, app(app(app(ty_@3, ce), cf), cg)), cd)) → new_lt0(vyw4310, vyw4510, ce, cf, cg)
new_ltEs3(Left(vyw4310), Left(vyw4510), app(ty_[], bda), bce) → new_ltEs1(vyw4310, vyw4510, bda)
new_compare20(@2(:(vyw4300, vyw4301), vyw431), @2(:(vyw4500, vyw4501), vyw451), False, app(ty_[], he), beg) → new_compare(vyw4301, vyw4501, he)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, app(app(app(ty_@3, ge), gf), gg)), df), fb)) → new_lt0(vyw4310, vyw4510, ge, gf, gg)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), app(app(ty_Either, ga), gb)), fb)) → new_lt3(vyw4311, vyw4511, ga, gb)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(app(ty_Either, hb), hc), df, fb) → new_lt3(vyw4310, vyw4510, hb, hc)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, app(ty_Maybe, fh), fb) → new_lt2(vyw4311, vyw4511, fh)
new_compare20(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(app(ty_@2, bag), bah), beg) → new_compare20(vyw430, vyw450, new_esEs4(vyw430, vyw450, bag, bah), bag, bah)
new_compare1(vyw430, vyw450, bag, bah) → new_compare20(vyw430, vyw450, new_esEs4(vyw430, vyw450, bag, bah), bag, bah)
new_primCompAux(vyw4300, vyw4500, vyw107, app(app(ty_@2, hf), hg)) → new_compare1(vyw4300, vyw4500, hf, hg)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, h), app(app(app(ty_@3, bc), bd), be))) → new_ltEs0(vyw4311, vyw4511, bc, bd, be)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, app(ty_[], fg), fb) → new_lt1(vyw4311, vyw4511, fg)
new_compare20(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bba, app(app(ty_Either, app(ty_[], bda)), bce)) → new_ltEs1(vyw4310, vyw4510, bda)
new_compare20(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bba, app(app(ty_Either, bde), app(app(app(ty_@3, bdh), bea), beb))) → new_ltEs0(vyw4310, vyw4510, bdh, bea, beb)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(app(ty_@2, gc), gd), df, fb) → new_lt(vyw4310, vyw4510, gc, gd)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, df, app(app(ty_Either, ef), eg)) → new_ltEs3(vyw4312, vyw4512, ef, eg)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, app(ty_Maybe, ha)), df), fb)) → new_lt2(vyw4310, vyw4510, ha)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), df), app(ty_Maybe, ee))) → new_ltEs2(vyw4312, vyw4512, ee)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, h), app(ty_Maybe, bg))) → new_ltEs2(vyw4311, vyw4511, bg)
new_compare20(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bba, app(ty_Maybe, app(app(ty_@2, bbb), bbc))) → new_ltEs(vyw4310, vyw4510, bbb, bbc)
new_compare20(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bba, app(app(ty_Either, bde), app(ty_Maybe, bed))) → new_ltEs2(vyw4310, vyw4510, bed)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, app(ty_[], da)), cd)) → new_lt1(vyw4310, vyw4510, da)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), h, app(ty_[], bf)) → new_ltEs1(vyw4311, vyw4511, bf)
new_ltEs1(vyw431, vyw451, hd) → new_compare(vyw431, vyw451, hd)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(app(app(ty_@3, ge), gf), gg), df, fb) → new_lt0(vyw4310, vyw4510, ge, gf, gg)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(ty_Maybe, db), cd) → new_lt2(vyw4310, vyw4510, db)
new_compare20(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bba, app(app(ty_Either, bde), app(app(ty_Either, bee), bef))) → new_ltEs3(vyw4310, vyw4510, bee, bef)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), app(ty_[], fg)), fb)) → new_lt1(vyw4311, vyw4511, fg)
new_compare20(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bba, app(ty_Maybe, app(ty_Maybe, bbh))) → new_ltEs2(vyw4310, vyw4510, bbh)
new_ltEs2(Just(vyw4310), Just(vyw4510), app(app(ty_Either, bca), bcb)) → new_ltEs3(vyw4310, vyw4510, bca, bcb)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(app(ty_@2, cb), cc), cd) → new_lt(vyw4310, vyw4510, cb, cc)
new_lt3(vyw430, vyw450, bfd, bfe) → new_compare23(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfd, bfe), bfd, bfe)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(app(app(ty_@3, ce), cf), cg), cd) → new_lt0(vyw4310, vyw4510, ce, cf, cg)
new_compare20(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bba, app(app(ty_Either, app(ty_Maybe, bdb)), bce)) → new_ltEs2(vyw4310, vyw4510, bdb)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, app(app(app(ty_@3, fc), fd), ff), fb) → new_lt0(vyw4311, vyw4511, fc, fd, ff)
new_compare20(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bba, app(ty_Maybe, app(app(ty_Either, bca), bcb))) → new_ltEs3(vyw4310, vyw4510, bca, bcb)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(ty_[], da), cd) → new_lt1(vyw4310, vyw4510, da)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), df), app(app(app(ty_@3, ea), eb), ec))) → new_ltEs0(vyw4312, vyw4512, ea, eb, ec)
new_primCompAux(vyw4300, vyw4500, vyw107, app(app(ty_Either, bae), baf)) → new_compare4(vyw4300, vyw4500, bae, baf)
new_ltEs3(Left(vyw4310), Left(vyw4510), app(app(ty_@2, bcc), bcd), bce) → new_ltEs(vyw4310, vyw4510, bcc, bcd)
new_lt2(vyw430, vyw450, bfc) → new_compare22(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfc), bfc)
new_compare20(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bba, app(app(ty_Either, app(app(ty_Either, bdc), bdd)), bce)) → new_ltEs3(vyw4310, vyw4510, bdc, bdd)
new_ltEs3(Right(vyw4310), Right(vyw4510), bde, app(ty_Maybe, bed)) → new_ltEs2(vyw4310, vyw4510, bed)
new_ltEs3(Right(vyw4310), Right(vyw4510), bde, app(ty_[], bec)) → new_ltEs1(vyw4310, vyw4510, bec)
new_compare22(vyw430, vyw450, False, bfc) → new_ltEs2(vyw430, vyw450, bfc)
new_compare20(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bba, app(app(ty_Either, bde), app(app(ty_@2, bdf), bdg))) → new_ltEs(vyw4310, vyw4510, bdf, bdg)
new_ltEs2(Just(vyw4310), Just(vyw4510), app(app(ty_@2, bbb), bbc)) → new_ltEs(vyw4310, vyw4510, bbb, bbc)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, df, app(ty_Maybe, ee)) → new_ltEs2(vyw4312, vyw4512, ee)
new_compare20(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bba, app(app(app(ty_@3, de), app(app(ty_@2, eh), fa)), fb)) → new_lt(vyw4311, vyw4511, eh, fa)
new_compare20(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bba, app(app(ty_Either, app(app(app(ty_@3, bcf), bcg), bch)), bce)) → new_ltEs0(vyw4310, vyw4510, bcf, bcg, bch)
new_compare21(vyw430, vyw450, False, beh, bfa, bfb) → new_ltEs0(vyw430, vyw450, beh, bfa, bfb)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, h), app(ty_[], bf))) → new_ltEs1(vyw4311, vyw4511, bf)
new_ltEs2(Just(vyw4310), Just(vyw4510), app(ty_Maybe, bbh)) → new_ltEs2(vyw4310, vyw4510, bbh)
new_compare(:(vyw4300, vyw4301), :(vyw4500, vyw4501), he) → new_compare(vyw4301, vyw4501, he)
new_compare(:(vyw4300, vyw4301), :(vyw4500, vyw4501), he) → new_primCompAux(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, he), he)
new_ltEs3(Right(vyw4310), Right(vyw4510), bde, app(app(ty_@2, bdf), bdg)) → new_ltEs(vyw4310, vyw4510, bdf, bdg)
new_compare20(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(app(ty_Either, bfd), bfe), beg) → new_compare23(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfd, bfe), bfd, bfe)
new_primCompAux(vyw4300, vyw4500, vyw107, app(app(app(ty_@3, hh), baa), bab)) → new_compare2(vyw4300, vyw4500, hh, baa, bab)
new_compare20(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bba, app(app(ty_@2, app(ty_Maybe, db)), cd)) → new_lt2(vyw4310, vyw4510, db)
new_compare20(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bba, app(ty_Maybe, app(ty_[], bbg))) → new_ltEs1(vyw4310, vyw4510, bbg)
new_compare4(vyw430, vyw450, bfd, bfe) → new_compare23(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfd, bfe), bfd, bfe)
new_ltEs0(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, app(app(ty_Either, ga), gb), fb) → new_lt3(vyw4311, vyw4511, ga, gb)
new_ltEs(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), h, app(app(app(ty_@3, bc), bd), be)) → new_ltEs0(vyw4311, vyw4511, bc, bd, be)
new_ltEs3(Left(vyw4310), Left(vyw4510), app(ty_Maybe, bdb), bce) → new_ltEs2(vyw4310, vyw4510, bdb)
new_ltEs3(Left(vyw4310), Left(vyw4510), app(app(app(ty_@3, bcf), bcg), bch), bce) → new_ltEs0(vyw4310, vyw4510, bcf, bcg, bch)
new_compare3(vyw430, vyw450, bfc) → new_compare22(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfc), bfc)
new_compare20(@2(vyw430, vyw431), @2(vyw450, vyw451), False, bba, app(ty_[], hd)) → new_compare(vyw431, vyw451, hd)
new_primCompAux(vyw4300, vyw4500, vyw107, app(ty_Maybe, bad)) → new_compare3(vyw4300, vyw4500, bad)

The TRS R consists of the following rules:

new_esEs23(vyw401, vyw3001, app(app(ty_Either, cee), cef)) → new_esEs7(vyw401, vyw3001, cee, cef)
new_lt4(vyw430, vyw450) → new_esEs8(new_compare5(vyw430, vyw450), LT)
new_compare17(Char(vyw4300), Char(vyw4500)) → new_primCmpNat0(vyw4300, vyw4500)
new_esEs7(Left(vyw400), Left(vyw3000), app(app(ty_Either, chb), chc), cgg) → new_esEs7(vyw400, vyw3000, chb, chc)
new_lt8(vyw4311, vyw4511, app(ty_Maybe, fh)) → new_lt17(vyw4311, vyw4511, fh)
new_esEs25(vyw401, vyw3001, ty_Integer) → new_esEs12(vyw401, vyw3001)
new_ltEs10(vyw4312, vyw4512, app(ty_Maybe, ee)) → new_ltEs6(vyw4312, vyw4512, ee)
new_ltEs11(LT, GT) → True
new_esEs24(vyw400, vyw3000, app(app(app(ty_@3, cga), cgb), cgc)) → new_esEs5(vyw400, vyw3000, cga, cgb, cgc)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Char) → new_ltEs14(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, app(app(ty_Either, bfd), bfe)) → new_lt19(vyw430, vyw450, bfd, bfe)
new_compare7(Double(vyw4300, vyw4301), Double(vyw4500, vyw4501)) → new_compare5(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_esEs7(Right(vyw400), Right(vyw3000), dab, app(ty_[], dbd)) → new_esEs17(vyw400, vyw3000, dbd)
new_esEs23(vyw401, vyw3001, app(app(ty_@2, cfb), cfc)) → new_esEs4(vyw401, vyw3001, cfb, cfc)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Int, cgg) → new_esEs9(vyw400, vyw3000)
new_esEs18(vyw401, vyw3001, app(ty_[], caf)) → new_esEs17(vyw401, vyw3001, caf)
new_esEs23(vyw401, vyw3001, ty_Bool) → new_esEs14(vyw401, vyw3001)
new_lt21(vyw4310, vyw4510, ty_@0) → new_lt18(vyw4310, vyw4510)
new_ltEs6(Nothing, Just(vyw4510), dbf) → True
new_esEs29(vyw4310, vyw4510, ty_Int) → new_esEs9(vyw4310, vyw4510)
new_esEs20(vyw4311, vyw4511, ty_Int) → new_esEs9(vyw4311, vyw4511)
new_esEs23(vyw401, vyw3001, app(ty_[], cfd)) → new_esEs17(vyw401, vyw3001, cfd)
new_lt21(vyw4310, vyw4510, ty_Ordering) → new_lt10(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_@0) → new_lt18(vyw430, vyw450)
new_ltEs8(vyw431, vyw451) → new_not(new_esEs8(new_compare5(vyw431, vyw451), GT))
new_primMulNat0(Zero, Zero) → Zero
new_esEs7(Left(vyw400), Left(vyw3000), app(app(app(ty_@3, chd), che), chf), cgg) → new_esEs5(vyw400, vyw3000, chd, che, chf)
new_lt9(vyw4310, vyw4510, ty_Ordering) → new_lt10(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Double) → new_esEs16(vyw400, vyw3000)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(app(ty_@2, bcc), bcd), bce) → new_ltEs12(vyw4310, vyw4510, bcc, bcd)
new_esEs28(vyw400, vyw3000, app(ty_Ratio, dcd)) → new_esEs10(vyw400, vyw3000, dcd)
new_sr(Integer(vyw43000), Integer(vyw45010)) → Integer(new_primMulInt(vyw43000, vyw45010))
new_lt21(vyw4310, vyw4510, ty_Float) → new_lt15(vyw4310, vyw4510)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Bool, cgg) → new_esEs14(vyw400, vyw3000)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_esEs27(vyw430, vyw450, ty_Integer) → new_esEs12(vyw430, vyw450)
new_lt8(vyw4311, vyw4511, ty_@0) → new_lt18(vyw4311, vyw4511)
new_ltEs10(vyw4312, vyw4512, ty_@0) → new_ltEs17(vyw4312, vyw4512)
new_ltEs20(vyw4311, vyw4511, ty_Char) → new_ltEs14(vyw4311, vyw4511)
new_lt9(vyw4310, vyw4510, ty_Double) → new_lt6(vyw4310, vyw4510)
new_ltEs7(True, True) → True
new_compare9(vyw4300, vyw4500, ty_Integer) → new_compare6(vyw4300, vyw4500)
new_lt21(vyw4310, vyw4510, ty_Char) → new_lt14(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(ty_[], da)) → new_lt16(vyw4310, vyw4510, da)
new_lt21(vyw4310, vyw4510, ty_Bool) → new_lt11(vyw4310, vyw4510)
new_esEs10(:%(vyw400, vyw401), :%(vyw3000, vyw3001), dbe) → new_asAs(new_esEs26(vyw400, vyw3000, dbe), new_esEs25(vyw401, vyw3001, dbe))
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Bool) → new_ltEs7(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Right(vyw3000), dab, app(app(app(ty_@3, dag), dah), dba)) → new_esEs5(vyw400, vyw3000, dag, dah, dba)
new_esEs19(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_ltEs20(vyw4311, vyw4511, app(app(ty_@2, ba), bb)) → new_ltEs12(vyw4311, vyw4511, ba, bb)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(app(ty_Either, bdc), bdd), bce) → new_ltEs18(vyw4310, vyw4510, bdc, bdd)
new_compare0(:(vyw4300, vyw4301), :(vyw4500, vyw4501), he) → new_primCompAux0(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, he), he)
new_lt9(vyw4310, vyw4510, app(ty_Maybe, ha)) → new_lt17(vyw4310, vyw4510, ha)
new_esEs22(vyw402, vyw3002, app(ty_Maybe, cdb)) → new_esEs6(vyw402, vyw3002, cdb)
new_esEs27(vyw430, vyw450, app(ty_Maybe, bfc)) → new_esEs6(vyw430, vyw450, bfc)
new_esEs29(vyw4310, vyw4510, ty_Char) → new_esEs11(vyw4310, vyw4510)
new_compare27(vyw430, vyw450, False, beh, bfa, bfb) → new_compare11(vyw430, vyw450, new_ltEs9(vyw430, vyw450, beh, bfa, bfb), beh, bfa, bfb)
new_ltEs18(Right(vyw4310), Left(vyw4510), bde, bce) → False
new_esEs23(vyw401, vyw3001, ty_Integer) → new_esEs12(vyw401, vyw3001)
new_esEs12(Integer(vyw400), Integer(vyw3000)) → new_primEqInt(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, app(app(app(ty_@3, cbc), cbd), cbe)) → new_esEs5(vyw400, vyw3000, cbc, cbd, cbe)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(app(app(ty_@3, bcf), bcg), bch), bce) → new_ltEs9(vyw4310, vyw4510, bcf, bcg, bch)
new_esEs28(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs28(vyw400, vyw3000, app(app(app(ty_@3, dch), dda), ddb)) → new_esEs5(vyw400, vyw3000, dch, dda, ddb)
new_esEs22(vyw402, vyw3002, app(app(ty_Either, cdc), cdd)) → new_esEs7(vyw402, vyw3002, cdc, cdd)
new_lt9(vyw4310, vyw4510, ty_@0) → new_lt18(vyw4310, vyw4510)
new_compare210(vyw430, vyw450, False) → new_compare114(vyw430, vyw450, new_ltEs11(vyw430, vyw450))
new_lt21(vyw4310, vyw4510, app(app(ty_@2, cb), cc)) → new_lt12(vyw4310, vyw4510, cb, cc)
new_esEs7(Right(vyw400), Right(vyw3000), dab, app(ty_Maybe, dad)) → new_esEs6(vyw400, vyw3000, dad)
new_ltEs10(vyw4312, vyw4512, ty_Int) → new_ltEs8(vyw4312, vyw4512)
new_lt9(vyw4310, vyw4510, app(app(ty_Either, hb), hc)) → new_lt19(vyw4310, vyw4510, hb, hc)
new_esEs13(Float(vyw400, vyw401), Float(vyw3000, vyw3001)) → new_esEs9(new_sr0(vyw400, vyw3000), new_sr0(vyw401, vyw3001))
new_ltEs7(True, False) → False
new_pePe(False, vyw106) → vyw106
new_compare114(vyw430, vyw450, False) → GT
new_esEs29(vyw4310, vyw4510, ty_Double) → new_esEs16(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Left(vyw3000), dab, cgg) → False
new_esEs7(Left(vyw400), Right(vyw3000), dab, cgg) → False
new_lt20(vyw430, vyw450, ty_Bool) → new_lt11(vyw430, vyw450)
new_ltEs7(False, True) → True
new_esEs19(vyw400, vyw3000, ty_@0) → new_esEs15(vyw400, vyw3000)
new_compare9(vyw4300, vyw4500, ty_Double) → new_compare7(vyw4300, vyw4500)
new_esEs20(vyw4311, vyw4511, ty_Double) → new_esEs16(vyw4311, vyw4511)
new_esEs27(vyw430, vyw450, app(app(ty_Either, bfd), bfe)) → new_esEs7(vyw430, vyw450, bfd, bfe)
new_esEs19(vyw400, vyw3000, app(ty_Maybe, cah)) → new_esEs6(vyw400, vyw3000, cah)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(app(ty_@3, bbd), bbe), bbf)) → new_ltEs9(vyw4310, vyw4510, bbd, bbe, bbf)
new_esEs22(vyw402, vyw3002, ty_@0) → new_esEs15(vyw402, vyw3002)
new_esEs22(vyw402, vyw3002, app(app(ty_@2, cdh), cea)) → new_esEs4(vyw402, vyw3002, cdh, cea)
new_esEs22(vyw402, vyw3002, ty_Integer) → new_esEs12(vyw402, vyw3002)
new_lt20(vyw430, vyw450, app(app(app(ty_@3, beh), bfa), bfb)) → new_lt13(vyw430, vyw450, beh, bfa, bfb)
new_esEs28(vyw400, vyw3000, ty_@0) → new_esEs15(vyw400, vyw3000)
new_ltEs20(vyw4311, vyw4511, ty_Double) → new_ltEs5(vyw4311, vyw4511)
new_compare11(vyw430, vyw450, False, beh, bfa, bfb) → GT
new_esEs27(vyw430, vyw450, app(ty_[], he)) → new_esEs17(vyw430, vyw450, he)
new_esEs22(vyw402, vyw3002, ty_Ordering) → new_esEs8(vyw402, vyw3002)
new_esEs19(vyw400, vyw3000, app(app(ty_Either, cba), cbb)) → new_esEs7(vyw400, vyw3000, cba, cbb)
new_ltEs10(vyw4312, vyw4512, ty_Double) → new_ltEs5(vyw4312, vyw4512)
new_compare10(vyw430, vyw450, True, bfc) → LT
new_esEs29(vyw4310, vyw4510, app(app(ty_@2, cb), cc)) → new_esEs4(vyw4310, vyw4510, cb, cc)
new_ltEs19(vyw431, vyw451, ty_Int) → new_ltEs8(vyw431, vyw451)
new_esEs6(Just(vyw400), Just(vyw3000), app(app(app(ty_@3, bgc), bgd), bge)) → new_esEs5(vyw400, vyw3000, bgc, bgd, bge)
new_primCmpNat0(Zero, Succ(vyw45000)) → LT
new_esEs21(vyw4310, vyw4510, ty_Bool) → new_esEs14(vyw4310, vyw4510)
new_ltEs19(vyw431, vyw451, ty_Float) → new_ltEs15(vyw431, vyw451)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Bool) → new_ltEs7(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Ratio, dbg)) → new_ltEs13(vyw4310, vyw4510, dbg)
new_esEs8(LT, LT) → True
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, app(app(ty_Either, bee), bef)) → new_ltEs18(vyw4310, vyw4510, bee, bef)
new_esEs19(vyw400, vyw3000, app(ty_[], cbh)) → new_esEs17(vyw400, vyw3000, cbh)
new_compare25(vyw430, vyw450, bfd, bfe) → new_compare28(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfd, bfe), bfd, bfe)
new_esEs28(vyw400, vyw3000, ty_Double) → new_esEs16(vyw400, vyw3000)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Float, cgg) → new_esEs13(vyw400, vyw3000)
new_compare10(vyw430, vyw450, False, bfc) → GT
new_esEs24(vyw400, vyw3000, app(app(ty_Either, cfg), cfh)) → new_esEs7(vyw400, vyw3000, cfg, cfh)
new_pePe(True, vyw106) → True
new_compare0([], [], he) → EQ
new_primEqNat0(Zero, Zero) → True
new_compare26(vyw430, vyw450, True) → EQ
new_esEs29(vyw4310, vyw4510, app(ty_Maybe, db)) → new_esEs6(vyw4310, vyw4510, db)
new_compare29(vyw43, vyw45, True, bba, beg) → EQ
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_@0) → new_ltEs17(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Integer) → new_lt7(vyw430, vyw450)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Ordering, cgg) → new_esEs8(vyw400, vyw3000)
new_compare24(vyw430, vyw450, False, bfc) → new_compare10(vyw430, vyw450, new_ltEs6(vyw430, vyw450, bfc), bfc)
new_esEs19(vyw400, vyw3000, ty_Float) → new_esEs13(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_[], bbg)) → new_ltEs16(vyw4310, vyw4510, bbg)
new_compare16(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Integer) → new_compare6(new_sr(vyw4300, vyw4501), new_sr(vyw4500, vyw4301))
new_esEs18(vyw401, vyw3001, app(app(app(ty_@3, caa), cab), cac)) → new_esEs5(vyw401, vyw3001, caa, cab, cac)
new_esEs24(vyw400, vyw3000, ty_Double) → new_esEs16(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Integer) → new_ltEs4(vyw4310, vyw4510)
new_esEs8(GT, GT) → True
new_esEs21(vyw4310, vyw4510, ty_Double) → new_esEs16(vyw4310, vyw4510)
new_primPlusNat0(Succ(vyw790), vyw300000) → Succ(Succ(new_primPlusNat1(vyw790, vyw300000)))
new_ltEs15(vyw431, vyw451) → new_not(new_esEs8(new_compare18(vyw431, vyw451), GT))
new_ltEs10(vyw4312, vyw4512, ty_Integer) → new_ltEs4(vyw4312, vyw4512)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Float) → new_ltEs15(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Right(vyw3000), dab, app(app(ty_Either, dae), daf)) → new_esEs7(vyw400, vyw3000, dae, daf)
new_compare9(vyw4300, vyw4500, app(app(app(ty_@3, hh), baa), bab)) → new_compare15(vyw4300, vyw4500, hh, baa, bab)
new_lt15(vyw430, vyw450) → new_esEs8(new_compare18(vyw430, vyw450), LT)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_lt9(vyw4310, vyw4510, ty_Integer) → new_lt7(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_Either, bca), bcb)) → new_ltEs18(vyw4310, vyw4510, bca, bcb)
new_lt16(vyw430, vyw450, he) → new_esEs8(new_compare0(vyw430, vyw450, he), LT)
new_esEs26(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_@0) → new_esEs15(vyw400, vyw3000)
new_primEqInt(Neg(Succ(vyw4000)), Neg(Succ(vyw30000))) → new_primEqNat0(vyw4000, vyw30000)
new_ltEs5(vyw431, vyw451) → new_not(new_esEs8(new_compare7(vyw431, vyw451), GT))
new_esEs7(Left(vyw400), Left(vyw3000), ty_Char, cgg) → new_esEs11(vyw400, vyw3000)
new_compare9(vyw4300, vyw4500, ty_Char) → new_compare17(vyw4300, vyw4500)
new_esEs20(vyw4311, vyw4511, ty_Ordering) → new_esEs8(vyw4311, vyw4511)
new_ltEs19(vyw431, vyw451, ty_Double) → new_ltEs5(vyw431, vyw451)
new_esEs23(vyw401, vyw3001, ty_Ordering) → new_esEs8(vyw401, vyw3001)
new_ltEs19(vyw431, vyw451, app(app(app(ty_@3, de), df), fb)) → new_ltEs9(vyw431, vyw451, de, df, fb)
new_esEs24(vyw400, vyw3000, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, app(ty_Ratio, dcb)) → new_ltEs13(vyw4310, vyw4510, dcb)
new_ltEs20(vyw4311, vyw4511, app(app(app(ty_@3, bc), bd), be)) → new_ltEs9(vyw4311, vyw4511, bc, bd, be)
new_primPlusNat1(Zero, Succ(vyw3000000)) → Succ(vyw3000000)
new_primPlusNat1(Succ(vyw7900), Zero) → Succ(vyw7900)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, app(app(ty_@2, bdf), bdg)) → new_ltEs12(vyw4310, vyw4510, bdf, bdg)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Float, bce) → new_ltEs15(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Int) → new_lt4(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, ty_@0) → new_esEs15(vyw4310, vyw4510)
new_esEs7(Left(vyw400), Left(vyw3000), app(ty_[], daa), cgg) → new_esEs17(vyw400, vyw3000, daa)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Float) → new_esEs13(vyw400, vyw3000)
new_lt9(vyw4310, vyw4510, app(app(ty_@2, gc), gd)) → new_lt12(vyw4310, vyw4510, gc, gd)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Double) → new_ltEs5(vyw4310, vyw4510)
new_compare111(vyw88, vyw89, vyw90, vyw91, True, ccd, cce) → LT
new_lt7(vyw430, vyw450) → new_esEs8(new_compare6(vyw430, vyw450), LT)
new_lt17(vyw430, vyw450, bfc) → new_esEs8(new_compare8(vyw430, vyw450, bfc), LT)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vyw401, vyw3001, ty_Char) → new_esEs11(vyw401, vyw3001)
new_compare11(vyw430, vyw450, True, beh, bfa, bfb) → LT
new_ltEs10(vyw4312, vyw4512, ty_Char) → new_ltEs14(vyw4312, vyw4512)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_esEs20(vyw4311, vyw4511, ty_Float) → new_esEs13(vyw4311, vyw4511)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Float) → new_esEs13(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_compare8(vyw430, vyw450, bfc) → new_compare24(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfc), bfc)
new_compare112(vyw430, vyw450, False, bfd, bfe) → GT
new_ltEs19(vyw431, vyw451, ty_Integer) → new_ltEs4(vyw431, vyw451)
new_primEqInt(Neg(Zero), Neg(Succ(vyw30000))) → False
new_primEqInt(Neg(Succ(vyw4000)), Neg(Zero)) → False
new_esEs8(EQ, EQ) → True
new_ltEs18(Left(vyw4310), Right(vyw4510), bde, bce) → True
new_compare9(vyw4300, vyw4500, ty_Float) → new_compare18(vyw4300, vyw4500)
new_esEs22(vyw402, vyw3002, ty_Float) → new_esEs13(vyw402, vyw3002)
new_ltEs10(vyw4312, vyw4512, ty_Float) → new_ltEs15(vyw4312, vyw4512)
new_esEs22(vyw402, vyw3002, app(app(app(ty_@3, cde), cdf), cdg)) → new_esEs5(vyw402, vyw3002, cde, cdf, cdg)
new_ltEs10(vyw4312, vyw4512, app(app(app(ty_@3, ea), eb), ec)) → new_ltEs9(vyw4312, vyw4512, ea, eb, ec)
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_lt5(vyw430, vyw450, bhb) → new_esEs8(new_compare16(vyw430, vyw450, bhb), LT)
new_ltEs20(vyw4311, vyw4511, app(app(ty_Either, bh), ca)) → new_ltEs18(vyw4311, vyw4511, bh, ca)
new_lt9(vyw4310, vyw4510, ty_Char) → new_lt14(vyw4310, vyw4510)
new_esEs29(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_primCmpNat0(Succ(vyw43000), Succ(vyw45000)) → new_primCmpNat0(vyw43000, vyw45000)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs7(Left(vyw400), Left(vyw3000), ty_@0, cgg) → new_esEs15(vyw400, vyw3000)
new_esEs18(vyw401, vyw3001, ty_Char) → new_esEs11(vyw401, vyw3001)
new_compare16(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Int) → new_compare5(new_sr0(vyw4300, vyw4501), new_sr0(vyw4500, vyw4301))
new_esEs6(Nothing, Nothing, bff) → True
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Integer, bce) → new_ltEs4(vyw4310, vyw4510)
new_esEs19(vyw400, vyw3000, ty_Char) → new_esEs11(vyw400, vyw3000)
new_lt21(vyw4310, vyw4510, app(ty_Ratio, ddg)) → new_lt5(vyw4310, vyw4510, ddg)
new_primEqInt(Pos(Succ(vyw4000)), Pos(Succ(vyw30000))) → new_primEqNat0(vyw4000, vyw30000)
new_ltEs10(vyw4312, vyw4512, app(app(ty_@2, dg), dh)) → new_ltEs12(vyw4312, vyw4512, dg, dh)
new_esEs18(vyw401, vyw3001, ty_@0) → new_esEs15(vyw401, vyw3001)
new_compare9(vyw4300, vyw4500, app(ty_Maybe, bad)) → new_compare8(vyw4300, vyw4500, bad)
new_esEs21(vyw4310, vyw4510, app(ty_Maybe, ha)) → new_esEs6(vyw4310, vyw4510, ha)
new_lt12(vyw430, vyw450, bag, bah) → new_esEs8(new_compare14(vyw430, vyw450, bag, bah), LT)
new_esEs14(True, False) → False
new_esEs14(False, True) → False
new_compare9(vyw4300, vyw4500, app(ty_[], bac)) → new_compare0(vyw4300, vyw4500, bac)
new_esEs25(vyw401, vyw3001, ty_Int) → new_esEs9(vyw401, vyw3001)
new_lt9(vyw4310, vyw4510, app(ty_[], gh)) → new_lt16(vyw4310, vyw4510, gh)
new_compare9(vyw4300, vyw4500, ty_Ordering) → new_compare12(vyw4300, vyw4500)
new_esEs6(Nothing, Just(vyw3000), bff) → False
new_esEs6(Just(vyw400), Nothing, bff) → False
new_primEqNat0(Succ(vyw4000), Succ(vyw30000)) → new_primEqNat0(vyw4000, vyw30000)
new_esEs27(vyw430, vyw450, ty_Ordering) → new_esEs8(vyw430, vyw450)
new_compare9(vyw4300, vyw4500, app(app(ty_@2, hf), hg)) → new_compare14(vyw4300, vyw4500, hf, hg)
new_lt8(vyw4311, vyw4511, ty_Bool) → new_lt11(vyw4311, vyw4511)
new_lt14(vyw430, vyw450) → new_esEs8(new_compare17(vyw430, vyw450), LT)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Char, bce) → new_ltEs14(vyw4310, vyw4510)
new_primCompAux00(vyw114, LT) → LT
new_ltEs17(vyw431, vyw451) → new_not(new_esEs8(new_compare19(vyw431, vyw451), GT))
new_lt9(vyw4310, vyw4510, app(app(app(ty_@3, ge), gf), gg)) → new_lt13(vyw4310, vyw4510, ge, gf, gg)
new_primCmpInt(Neg(Succ(vyw43000)), Neg(vyw4500)) → new_primCmpNat0(vyw4500, Succ(vyw43000))
new_esEs4(@2(vyw400, vyw401), @2(vyw3000, vyw3001), bhc, bhd) → new_asAs(new_esEs19(vyw400, vyw3000, bhc), new_esEs18(vyw401, vyw3001, bhd))
new_esEs22(vyw402, vyw3002, ty_Bool) → new_esEs14(vyw402, vyw3002)
new_esEs24(vyw400, vyw3000, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_esEs27(vyw430, vyw450, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs5(vyw430, vyw450, beh, bfa, bfb)
new_lt13(vyw430, vyw450, beh, bfa, bfb) → new_esEs8(new_compare15(vyw430, vyw450, beh, bfa, bfb), LT)
new_esEs28(vyw400, vyw3000, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_lt20(vyw430, vyw450, app(ty_Ratio, bhb)) → new_lt5(vyw430, vyw450, bhb)
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(vyw30000))) → False
new_primEqInt(Pos(Succ(vyw4000)), Pos(Zero)) → False
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Ordering, bce) → new_ltEs11(vyw4310, vyw4510)
new_ltEs19(vyw431, vyw451, app(ty_Maybe, dbf)) → new_ltEs6(vyw431, vyw451, dbf)
new_compare19(@0, @0) → EQ
new_ltEs6(Just(vyw4310), Nothing, dbf) → False
new_primCmpNat0(Zero, Zero) → EQ
new_ltEs10(vyw4312, vyw4512, app(ty_Ratio, cca)) → new_ltEs13(vyw4312, vyw4512, cca)
new_ltEs11(GT, EQ) → False
new_primCmpNat0(Succ(vyw43000), Zero) → GT
new_lt19(vyw430, vyw450, bfd, bfe) → new_esEs8(new_compare25(vyw430, vyw450, bfd, bfe), LT)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(ty_Maybe, bdb), bce) → new_ltEs6(vyw4310, vyw4510, bdb)
new_ltEs19(vyw431, vyw451, app(ty_Ratio, dbh)) → new_ltEs13(vyw431, vyw451, dbh)
new_esEs24(vyw400, vyw3000, ty_@0) → new_esEs15(vyw400, vyw3000)
new_primCmpInt(Neg(Zero), Pos(Succ(vyw45000))) → LT
new_esEs23(vyw401, vyw3001, ty_Float) → new_esEs13(vyw401, vyw3001)
new_primPlusNat1(Succ(vyw7900), Succ(vyw3000000)) → Succ(Succ(new_primPlusNat1(vyw7900, vyw3000000)))
new_compare6(Integer(vyw4300), Integer(vyw4500)) → new_primCmpInt(vyw4300, vyw4500)
new_ltEs19(vyw431, vyw451, app(app(ty_@2, h), cd)) → new_ltEs12(vyw431, vyw451, h, cd)
new_compare28(vyw430, vyw450, True, bfd, bfe) → EQ
new_lt8(vyw4311, vyw4511, ty_Char) → new_lt14(vyw4311, vyw4511)
new_primEqInt(Neg(Succ(vyw4000)), Pos(vyw3000)) → False
new_primEqInt(Pos(Succ(vyw4000)), Neg(vyw3000)) → False
new_ltEs16(vyw431, vyw451, hd) → new_not(new_esEs8(new_compare0(vyw431, vyw451, hd), GT))
new_esEs24(vyw400, vyw3000, app(app(ty_@2, cgd), cge)) → new_esEs4(vyw400, vyw3000, cgd, cge)
new_ltEs20(vyw4311, vyw4511, ty_Integer) → new_ltEs4(vyw4311, vyw4511)
new_esEs18(vyw401, vyw3001, app(app(ty_@2, cad), cae)) → new_esEs4(vyw401, vyw3001, cad, cae)
new_esEs28(vyw400, vyw3000, ty_Char) → new_esEs11(vyw400, vyw3000)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Char) → new_esEs11(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Float) → new_ltEs15(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Maybe, bbh)) → new_ltEs6(vyw4310, vyw4510, bbh)
new_ltEs20(vyw4311, vyw4511, ty_Float) → new_ltEs15(vyw4311, vyw4511)
new_compare13(vyw430, vyw450) → new_compare26(vyw430, vyw450, new_esEs14(vyw430, vyw450))
new_esEs26(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs28(vyw400, vyw3000, app(ty_Maybe, dce)) → new_esEs6(vyw400, vyw3000, dce)
new_ltEs11(GT, LT) → False
new_primEqInt(Neg(Zero), Pos(Succ(vyw30000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vyw30000))) → False
new_primCompAux00(vyw114, EQ) → vyw114
new_esEs21(vyw4310, vyw4510, ty_Char) → new_esEs11(vyw4310, vyw4510)
new_primCmpInt(Pos(Zero), Pos(Succ(vyw45000))) → new_primCmpNat0(Zero, Succ(vyw45000))
new_compare15(vyw430, vyw450, beh, bfa, bfb) → new_compare27(vyw430, vyw450, new_esEs5(vyw430, vyw450, beh, bfa, bfb), beh, bfa, bfb)
new_esEs28(vyw400, vyw3000, app(app(ty_Either, dcf), dcg)) → new_esEs7(vyw400, vyw3000, dcf, dcg)
new_esEs23(vyw401, vyw3001, app(ty_Ratio, cec)) → new_esEs10(vyw401, vyw3001, cec)
new_lt8(vyw4311, vyw4511, app(app(ty_Either, ga), gb)) → new_lt19(vyw4311, vyw4511, ga, gb)
new_esEs7(Right(vyw400), Right(vyw3000), dab, app(ty_Ratio, dac)) → new_esEs10(vyw400, vyw3000, dac)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, app(app(app(ty_@3, bdh), bea), beb)) → new_ltEs9(vyw4310, vyw4510, bdh, bea, beb)
new_ltEs11(LT, EQ) → True
new_esEs27(vyw430, vyw450, ty_Double) → new_esEs16(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, app(ty_[], gh)) → new_esEs17(vyw4310, vyw4510, gh)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Int) → new_esEs9(vyw400, vyw3000)
new_ltEs11(LT, LT) → True
new_lt8(vyw4311, vyw4511, app(app(app(ty_@3, fc), fd), ff)) → new_lt13(vyw4311, vyw4511, fc, fd, ff)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Int, bce) → new_ltEs8(vyw4310, vyw4510)
new_not(False) → True
new_ltEs10(vyw4312, vyw4512, app(ty_[], ed)) → new_ltEs16(vyw4312, vyw4512, ed)
new_primCompAux0(vyw4300, vyw4500, vyw107, he) → new_primCompAux00(vyw107, new_compare9(vyw4300, vyw4500, he))
new_compare24(vyw430, vyw450, True, bfc) → EQ
new_esEs20(vyw4311, vyw4511, app(ty_Ratio, ccb)) → new_esEs10(vyw4311, vyw4511, ccb)
new_esEs7(Left(vyw400), Left(vyw3000), app(ty_Maybe, cha), cgg) → new_esEs6(vyw400, vyw3000, cha)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Double, cgg) → new_esEs16(vyw400, vyw3000)
new_esEs23(vyw401, vyw3001, ty_@0) → new_esEs15(vyw401, vyw3001)
new_primPlusNat0(Zero, vyw300000) → Succ(vyw300000)
new_primCmpInt(Pos(Succ(vyw43000)), Pos(vyw4500)) → new_primCmpNat0(Succ(vyw43000), vyw4500)
new_esEs29(vyw4310, vyw4510, ty_Integer) → new_esEs12(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(app(ty_Either, dc), dd)) → new_lt19(vyw4310, vyw4510, dc, dd)
new_esEs29(vyw4310, vyw4510, app(ty_[], da)) → new_esEs17(vyw4310, vyw4510, da)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Integer, cgg) → new_esEs12(vyw400, vyw3000)
new_compare113(vyw88, vyw89, vyw90, vyw91, True, vyw93, ccd, cce) → new_compare111(vyw88, vyw89, vyw90, vyw91, True, ccd, cce)
new_ltEs12(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), h, cd) → new_pePe(new_lt21(vyw4310, vyw4510, h), new_asAs(new_esEs29(vyw4310, vyw4510, h), new_ltEs20(vyw4311, vyw4511, cd)))
new_ltEs9(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), de, df, fb) → new_pePe(new_lt9(vyw4310, vyw4510, de), new_asAs(new_esEs21(vyw4310, vyw4510, de), new_pePe(new_lt8(vyw4311, vyw4511, df), new_asAs(new_esEs20(vyw4311, vyw4511, df), new_ltEs10(vyw4312, vyw4512, fb)))))
new_lt8(vyw4311, vyw4511, ty_Integer) → new_lt7(vyw4311, vyw4511)
new_lt20(vyw430, vyw450, app(ty_Maybe, bfc)) → new_lt17(vyw430, vyw450, bfc)
new_esEs24(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs7(Left(vyw400), Left(vyw3000), app(ty_Ratio, cgh), cgg) → new_esEs10(vyw400, vyw3000, cgh)
new_compare0(:(vyw4300, vyw4301), [], he) → GT
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Bool, bce) → new_ltEs7(vyw4310, vyw4510)
new_esEs24(vyw400, vyw3000, app(ty_[], cgf)) → new_esEs17(vyw400, vyw3000, cgf)
new_ltEs11(GT, GT) → True
new_lt20(vyw430, vyw450, ty_Double) → new_lt6(vyw430, vyw450)
new_ltEs10(vyw4312, vyw4512, ty_Ordering) → new_ltEs11(vyw4312, vyw4512)
new_ltEs19(vyw431, vyw451, app(app(ty_Either, bde), bce)) → new_ltEs18(vyw431, vyw451, bde, bce)
new_ltEs20(vyw4311, vyw4511, ty_@0) → new_ltEs17(vyw4311, vyw4511)
new_esEs20(vyw4311, vyw4511, app(app(app(ty_@3, fc), fd), ff)) → new_esEs5(vyw4311, vyw4511, fc, fd, ff)
new_lt8(vyw4311, vyw4511, ty_Ordering) → new_lt10(vyw4311, vyw4511)
new_primCmpInt(Pos(Succ(vyw43000)), Neg(vyw4500)) → GT
new_esEs22(vyw402, vyw3002, ty_Char) → new_esEs11(vyw402, vyw3002)
new_esEs18(vyw401, vyw3001, app(app(ty_Either, bhg), bhh)) → new_esEs7(vyw401, vyw3001, bhg, bhh)
new_esEs27(vyw430, vyw450, ty_@0) → new_esEs15(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, app(app(app(ty_@3, ge), gf), gg)) → new_esEs5(vyw4310, vyw4510, ge, gf, gg)
new_ltEs19(vyw431, vyw451, app(ty_[], hd)) → new_ltEs16(vyw431, vyw451, hd)
new_lt18(vyw430, vyw450) → new_esEs8(new_compare19(vyw430, vyw450), LT)
new_primMulInt(Pos(vyw4000), Pos(vyw30000)) → Pos(new_primMulNat0(vyw4000, vyw30000))
new_esEs21(vyw4310, vyw4510, app(app(ty_@2, gc), gd)) → new_esEs4(vyw4310, vyw4510, gc, gd)
new_esEs18(vyw401, vyw3001, ty_Float) → new_esEs13(vyw401, vyw3001)
new_esEs18(vyw401, vyw3001, ty_Int) → new_esEs9(vyw401, vyw3001)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, app(ty_[], bec)) → new_ltEs16(vyw4310, vyw4510, bec)
new_compare12(vyw430, vyw450) → new_compare210(vyw430, vyw450, new_esEs8(vyw430, vyw450))
new_esEs20(vyw4311, vyw4511, ty_Char) → new_esEs11(vyw4311, vyw4511)
new_primMulInt(Neg(vyw4000), Neg(vyw30000)) → Pos(new_primMulNat0(vyw4000, vyw30000))
new_esEs7(Right(vyw400), Right(vyw3000), dab, app(app(ty_@2, dbb), dbc)) → new_esEs4(vyw400, vyw3000, dbb, dbc)
new_compare110(vyw430, vyw450, True) → LT
new_lt8(vyw4311, vyw4511, app(app(ty_@2, eh), fa)) → new_lt12(vyw4311, vyw4511, eh, fa)
new_esEs21(vyw4310, vyw4510, app(ty_Ratio, ccc)) → new_esEs10(vyw4310, vyw4510, ccc)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_@0, bce) → new_ltEs17(vyw4310, vyw4510)
new_primEqNat0(Zero, Succ(vyw30000)) → False
new_primEqNat0(Succ(vyw4000), Zero) → False
new_esEs21(vyw4310, vyw4510, ty_Int) → new_esEs9(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, app(app(ty_@2, bag), bah)) → new_lt12(vyw430, vyw450, bag, bah)
new_esEs20(vyw4311, vyw4511, ty_Bool) → new_esEs14(vyw4311, vyw4511)
new_compare110(vyw430, vyw450, False) → GT
new_esEs20(vyw4311, vyw4511, ty_@0) → new_esEs15(vyw4311, vyw4511)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_ltEs18(Left(vyw4310), Left(vyw4510), app(ty_[], bda), bce) → new_ltEs16(vyw4310, vyw4510, bda)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_@0) → new_ltEs17(vyw4310, vyw4510)
new_esEs20(vyw4311, vyw4511, app(ty_[], fg)) → new_esEs17(vyw4311, vyw4511, fg)
new_esEs22(vyw402, vyw3002, ty_Int) → new_esEs9(vyw402, vyw3002)
new_compare210(vyw430, vyw450, True) → EQ
new_ltEs19(vyw431, vyw451, ty_Ordering) → new_ltEs11(vyw431, vyw451)
new_esEs22(vyw402, vyw3002, app(ty_[], ceb)) → new_esEs17(vyw402, vyw3002, ceb)
new_compare18(Float(vyw4300, vyw4301), Float(vyw4500, vyw4501)) → new_compare5(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_lt20(vyw430, vyw450, ty_Char) → new_lt14(vyw430, vyw450)
new_ltEs19(vyw431, vyw451, ty_@0) → new_ltEs17(vyw431, vyw451)
new_esEs21(vyw4310, vyw4510, app(app(ty_Either, hb), hc)) → new_esEs7(vyw4310, vyw4510, hb, hc)
new_ltEs20(vyw4311, vyw4511, app(ty_Maybe, bg)) → new_ltEs6(vyw4311, vyw4511, bg)
new_compare9(vyw4300, vyw4500, ty_Bool) → new_compare13(vyw4300, vyw4500)
new_esEs29(vyw4310, vyw4510, app(app(app(ty_@3, ce), cf), cg)) → new_esEs5(vyw4310, vyw4510, ce, cf, cg)
new_ltEs19(vyw431, vyw451, ty_Bool) → new_ltEs7(vyw431, vyw451)
new_esEs27(vyw430, vyw450, app(ty_Ratio, bhb)) → new_esEs10(vyw430, vyw450, bhb)
new_esEs24(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs18(vyw401, vyw3001, ty_Double) → new_esEs16(vyw401, vyw3001)
new_lt10(vyw430, vyw450) → new_esEs8(new_compare12(vyw430, vyw450), LT)
new_primCmpInt(Neg(Zero), Neg(Succ(vyw45000))) → new_primCmpNat0(Succ(vyw45000), Zero)
new_primCmpInt(Pos(Zero), Neg(Succ(vyw45000))) → GT
new_esEs7(Left(vyw400), Left(vyw3000), app(app(ty_@2, chg), chh), cgg) → new_esEs4(vyw400, vyw3000, chg, chh)
new_compare5(vyw430, vyw450) → new_primCmpInt(vyw430, vyw450)
new_esEs16(Double(vyw400, vyw401), Double(vyw3000, vyw3001)) → new_esEs9(new_sr0(vyw400, vyw3000), new_sr0(vyw401, vyw3001))
new_esEs29(vyw4310, vyw4510, ty_@0) → new_esEs15(vyw4310, vyw4510)
new_sr0(vyw400, vyw3000) → new_primMulInt(vyw400, vyw3000)
new_esEs27(vyw430, vyw450, ty_Int) → new_esEs9(vyw430, vyw450)
new_ltEs20(vyw4311, vyw4511, ty_Ordering) → new_ltEs11(vyw4311, vyw4511)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Double) → new_esEs16(vyw400, vyw3000)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Bool) → new_esEs14(vyw400, vyw3000)
new_lt8(vyw4311, vyw4511, ty_Int) → new_lt4(vyw4311, vyw4511)
new_ltEs19(vyw431, vyw451, ty_Char) → new_ltEs14(vyw431, vyw451)
new_esEs6(Just(vyw400), Just(vyw3000), app(ty_[], bgh)) → new_esEs17(vyw400, vyw3000, bgh)
new_esEs18(vyw401, vyw3001, ty_Integer) → new_esEs12(vyw401, vyw3001)
new_esEs11(Char(vyw400), Char(vyw3000)) → new_primEqNat0(vyw400, vyw3000)
new_lt8(vyw4311, vyw4511, ty_Float) → new_lt15(vyw4311, vyw4511)
new_ltEs20(vyw4311, vyw4511, app(ty_[], bf)) → new_ltEs16(vyw4311, vyw4511, bf)
new_esEs20(vyw4311, vyw4511, app(app(ty_Either, ga), gb)) → new_esEs7(vyw4311, vyw4511, ga, gb)
new_ltEs11(EQ, EQ) → True
new_lt11(vyw430, vyw450) → new_esEs8(new_compare13(vyw430, vyw450), LT)
new_esEs18(vyw401, vyw3001, app(ty_Maybe, bhf)) → new_esEs6(vyw401, vyw3001, bhf)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Double, bce) → new_ltEs5(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, app(ty_[], he)) → new_lt16(vyw430, vyw450, he)
new_lt8(vyw4311, vyw4511, app(ty_Ratio, ccb)) → new_lt5(vyw4311, vyw4511, ccb)
new_ltEs10(vyw4312, vyw4512, app(app(ty_Either, ef), eg)) → new_ltEs18(vyw4312, vyw4512, ef, eg)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Integer) → new_ltEs4(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, ty_Double) → new_lt6(vyw4310, vyw4510)
new_esEs21(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vyw430, vyw450, ty_Float) → new_esEs13(vyw430, vyw450)
new_lt8(vyw4311, vyw4511, ty_Double) → new_lt6(vyw4311, vyw4511)
new_esEs20(vyw4311, vyw4511, app(ty_Maybe, fh)) → new_esEs6(vyw4311, vyw4511, fh)
new_esEs24(vyw400, vyw3000, ty_Char) → new_esEs11(vyw400, vyw3000)
new_ltEs20(vyw4311, vyw4511, ty_Bool) → new_ltEs7(vyw4311, vyw4511)
new_esEs19(vyw400, vyw3000, ty_Double) → new_esEs16(vyw400, vyw3000)
new_esEs15(@0, @0) → True
new_esEs28(vyw400, vyw3000, app(app(ty_@2, ddc), ddd)) → new_esEs4(vyw400, vyw3000, ddc, ddd)
new_asAs(False, vyw60) → False
new_primMulInt(Neg(vyw4000), Pos(vyw30000)) → Neg(new_primMulNat0(vyw4000, vyw30000))
new_primMulInt(Pos(vyw4000), Neg(vyw30000)) → Neg(new_primMulNat0(vyw4000, vyw30000))
new_primMulNat0(Succ(vyw40000), Zero) → Zero
new_primMulNat0(Zero, Succ(vyw300000)) → Zero
new_esEs6(Just(vyw400), Just(vyw3000), app(ty_Maybe, bfh)) → new_esEs6(vyw400, vyw3000, bfh)
new_esEs21(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_compare29(@2(vyw430, vyw431), @2(vyw450, vyw451), False, bba, beg) → new_compare113(vyw430, vyw431, vyw450, vyw451, new_lt20(vyw430, vyw450, bba), new_asAs(new_esEs27(vyw430, vyw450, bba), new_ltEs19(vyw431, vyw451, beg)), bba, beg)
new_ltEs11(EQ, LT) → False
new_lt21(vyw4310, vyw4510, app(ty_Maybe, db)) → new_lt17(vyw4310, vyw4510, db)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Ordering) → new_ltEs11(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(app(app(ty_@3, ce), cf), cg)) → new_lt13(vyw4310, vyw4510, ce, cf, cg)
new_esEs23(vyw401, vyw3001, ty_Int) → new_esEs9(vyw401, vyw3001)
new_compare26(vyw430, vyw450, False) → new_compare110(vyw430, vyw450, new_ltEs7(vyw430, vyw450))
new_esEs28(vyw400, vyw3000, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(ty_Ratio, dca), bce) → new_ltEs13(vyw4310, vyw4510, dca)
new_esEs6(Just(vyw400), Just(vyw3000), app(app(ty_@2, bgf), bgg)) → new_esEs4(vyw400, vyw3000, bgf, bgg)
new_compare14(vyw430, vyw450, bag, bah) → new_compare29(vyw430, vyw450, new_esEs4(vyw430, vyw450, bag, bah), bag, bah)
new_compare28(vyw430, vyw450, False, bfd, bfe) → new_compare112(vyw430, vyw450, new_ltEs18(vyw430, vyw450, bfd, bfe), bfd, bfe)
new_esEs23(vyw401, vyw3001, app(ty_Maybe, ced)) → new_esEs6(vyw401, vyw3001, ced)
new_esEs18(vyw401, vyw3001, ty_Ordering) → new_esEs8(vyw401, vyw3001)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, app(ty_Maybe, bed)) → new_ltEs6(vyw4310, vyw4510, bed)
new_esEs28(vyw400, vyw3000, ty_Float) → new_esEs13(vyw400, vyw3000)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Char) → new_esEs11(vyw400, vyw3000)
new_esEs29(vyw4310, vyw4510, app(ty_Ratio, ddg)) → new_esEs10(vyw4310, vyw4510, ddg)
new_compare111(vyw88, vyw89, vyw90, vyw91, False, ccd, cce) → GT
new_compare9(vyw4300, vyw4500, app(app(ty_Either, bae), baf)) → new_compare25(vyw4300, vyw4500, bae, baf)
new_esEs24(vyw400, vyw3000, app(ty_Ratio, cfe)) → new_esEs10(vyw400, vyw3000, cfe)
new_lt8(vyw4311, vyw4511, app(ty_[], fg)) → new_lt16(vyw4311, vyw4511, fg)
new_esEs23(vyw401, vyw3001, ty_Double) → new_esEs16(vyw401, vyw3001)
new_esEs20(vyw4311, vyw4511, app(app(ty_@2, eh), fa)) → new_esEs4(vyw4311, vyw4511, eh, fa)
new_esEs14(True, True) → True
new_compare113(vyw88, vyw89, vyw90, vyw91, False, vyw93, ccd, cce) → new_compare111(vyw88, vyw89, vyw90, vyw91, vyw93, ccd, cce)
new_esEs27(vyw430, vyw450, ty_Bool) → new_esEs14(vyw430, vyw450)
new_esEs20(vyw4311, vyw4511, ty_Integer) → new_esEs12(vyw4311, vyw4511)
new_esEs5(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ccf, ccg, cch) → new_asAs(new_esEs24(vyw400, vyw3000, ccf), new_asAs(new_esEs23(vyw401, vyw3001, ccg), new_esEs22(vyw402, vyw3002, cch)))
new_esEs22(vyw402, vyw3002, app(ty_Ratio, cda)) → new_esEs10(vyw402, vyw3002, cda)
new_ltEs6(Nothing, Nothing, dbf) → True
new_ltEs4(vyw431, vyw451) → new_not(new_esEs8(new_compare6(vyw431, vyw451), GT))
new_esEs28(vyw400, vyw3000, app(ty_[], dde)) → new_esEs17(vyw400, vyw3000, dde)
new_esEs27(vyw430, vyw450, app(app(ty_@2, bag), bah)) → new_esEs4(vyw430, vyw450, bag, bah)
new_esEs7(Right(vyw400), Right(vyw3000), dab, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs6(Just(vyw400), Just(vyw3000), app(ty_Ratio, bfg)) → new_esEs10(vyw400, vyw3000, bfg)
new_esEs19(vyw400, vyw3000, app(ty_Ratio, cag)) → new_esEs10(vyw400, vyw3000, cag)
new_ltEs13(vyw431, vyw451, dbh) → new_not(new_esEs8(new_compare16(vyw431, vyw451, dbh), GT))
new_esEs6(Just(vyw400), Just(vyw3000), ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_lt21(vyw4310, vyw4510, ty_Int) → new_lt4(vyw4310, vyw4510)
new_lt6(vyw430, vyw450) → new_esEs8(new_compare7(vyw430, vyw450), LT)
new_compare9(vyw4300, vyw4500, app(ty_Ratio, bha)) → new_compare16(vyw4300, vyw4500, bha)
new_ltEs7(False, False) → True
new_ltEs14(vyw431, vyw451) → new_not(new_esEs8(new_compare17(vyw431, vyw451), GT))
new_esEs28(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs29(vyw4310, vyw4510, app(app(ty_Either, dc), dd)) → new_esEs7(vyw4310, vyw4510, dc, dd)
new_esEs14(False, False) → True
new_compare9(vyw4300, vyw4500, ty_Int) → new_compare5(vyw4300, vyw4500)
new_esEs22(vyw402, vyw3002, ty_Double) → new_esEs16(vyw402, vyw3002)
new_esEs18(vyw401, vyw3001, ty_Bool) → new_esEs14(vyw401, vyw3001)
new_esEs6(Just(vyw400), Just(vyw3000), ty_@0) → new_esEs15(vyw400, vyw3000)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Ordering) → new_ltEs11(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Ordering) → new_lt10(vyw430, vyw450)
new_primPlusNat1(Zero, Zero) → Zero
new_compare0([], :(vyw4500, vyw4501), he) → LT
new_lt21(vyw4310, vyw4510, ty_Integer) → new_lt7(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Float) → new_lt15(vyw430, vyw450)
new_asAs(True, vyw60) → vyw60
new_compare112(vyw430, vyw450, True, bfd, bfe) → LT
new_primMulNat0(Succ(vyw40000), Succ(vyw300000)) → new_primPlusNat0(new_primMulNat0(vyw40000, Succ(vyw300000)), vyw300000)
new_esEs17(:(vyw400, vyw401), :(vyw3000, vyw3001), dcc) → new_asAs(new_esEs28(vyw400, vyw3000, dcc), new_esEs17(vyw401, vyw3001, dcc))
new_esEs6(Just(vyw400), Just(vyw3000), app(app(ty_Either, bga), bgb)) → new_esEs7(vyw400, vyw3000, bga, bgb)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Char) → new_ltEs14(vyw4310, vyw4510)
new_compare27(vyw430, vyw450, True, beh, bfa, bfb) → EQ
new_esEs17([], [], dcc) → True
new_esEs24(vyw400, vyw3000, ty_Float) → new_esEs13(vyw400, vyw3000)
new_esEs17(:(vyw400, vyw401), [], dcc) → False
new_esEs17([], :(vyw3000, vyw3001), dcc) → False
new_lt9(vyw4310, vyw4510, ty_Int) → new_lt4(vyw4310, vyw4510)
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Double) → new_ltEs5(vyw4310, vyw4510)
new_esEs23(vyw401, vyw3001, app(app(app(ty_@3, ceg), ceh), cfa)) → new_esEs5(vyw401, vyw3001, ceg, ceh, cfa)
new_esEs19(vyw400, vyw3000, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Int) → new_ltEs8(vyw4310, vyw4510)
new_compare9(vyw4300, vyw4500, ty_@0) → new_compare19(vyw4300, vyw4500)
new_ltEs20(vyw4311, vyw4511, ty_Int) → new_ltEs8(vyw4311, vyw4511)
new_esEs21(vyw4310, vyw4510, ty_Integer) → new_esEs12(vyw4310, vyw4510)
new_lt9(vyw4310, vyw4510, app(ty_Ratio, ccc)) → new_lt5(vyw4310, vyw4510, ccc)
new_esEs9(vyw40, vyw300) → new_primEqInt(vyw40, vyw300)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_@2, bbb), bbc)) → new_ltEs12(vyw4310, vyw4510, bbb, bbc)
new_esEs24(vyw400, vyw3000, app(ty_Maybe, cff)) → new_esEs6(vyw400, vyw3000, cff)
new_ltEs10(vyw4312, vyw4512, ty_Bool) → new_ltEs7(vyw4312, vyw4512)
new_esEs27(vyw430, vyw450, ty_Char) → new_esEs11(vyw430, vyw450)
new_compare114(vyw430, vyw450, True) → LT
new_esEs29(vyw4310, vyw4510, ty_Bool) → new_esEs14(vyw4310, vyw4510)
new_lt9(vyw4310, vyw4510, ty_Bool) → new_lt11(vyw4310, vyw4510)
new_primCompAux00(vyw114, GT) → GT
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_lt9(vyw4310, vyw4510, ty_Float) → new_lt15(vyw4310, vyw4510)
new_esEs29(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_esEs19(vyw400, vyw3000, app(app(ty_@2, cbf), cbg)) → new_esEs4(vyw400, vyw3000, cbf, cbg)
new_ltEs11(EQ, GT) → True
new_esEs18(vyw401, vyw3001, app(ty_Ratio, bhe)) → new_esEs10(vyw401, vyw3001, bhe)
new_ltEs20(vyw4311, vyw4511, app(ty_Ratio, ddf)) → new_ltEs13(vyw4311, vyw4511, ddf)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_ltEs18(Right(vyw4310), Right(vyw4510), bde, ty_Int) → new_ltEs8(vyw4310, vyw4510)
new_primCmpInt(Neg(Succ(vyw43000)), Pos(vyw4500)) → LT
new_not(True) → False

The set Q consists of the following terms:

new_esEs7(Right(x0), Right(x1), x2, ty_Char)
new_compare0(:(x0, x1), :(x2, x3), x4)
new_esEs7(Right(x0), Right(x1), x2, ty_Int)
new_primCompAux00(x0, EQ)
new_compare110(x0, x1, True)
new_esEs20(x0, x1, ty_Bool)
new_esEs27(x0, x1, app(ty_[], x2))
new_ltEs18(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs29(x0, x1, app(ty_Ratio, x2))
new_ltEs20(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_ltEs11(EQ, GT)
new_ltEs11(GT, EQ)
new_ltEs4(x0, x1)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_lt8(x0, x1, ty_Int)
new_ltEs18(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_Integer)
new_lt21(x0, x1, app(app(ty_@2, x2), x3))
new_compare13(x0, x1)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt19(x0, x1, x2, x3)
new_esEs5(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_compare9(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs20(x0, x1, app(ty_[], x2))
new_esEs11(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs29(x0, x1, ty_Int)
new_ltEs19(x0, x1, ty_Bool)
new_ltEs11(EQ, EQ)
new_lt13(x0, x1, x2, x3, x4)
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs7(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs18(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Integer)
new_lt21(x0, x1, ty_Ordering)
new_esEs13(Float(x0, x1), Float(x2, x3))
new_lt18(x0, x1)
new_compare11(x0, x1, False, x2, x3, x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs21(x0, x1, ty_Float)
new_compare27(x0, x1, False, x2, x3, x4)
new_sr0(x0, x1)
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_lt9(x0, x1, ty_Char)
new_ltEs6(Just(x0), Nothing, x1)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_lt20(x0, x1, ty_Bool)
new_esEs7(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, ty_Integer)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_esEs8(GT, GT)
new_esEs7(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_lt20(x0, x1, ty_Float)
new_esEs18(x0, x1, app(ty_[], x2))
new_ltEs18(Left(x0), Right(x1), x2, x3)
new_ltEs18(Right(x0), Left(x1), x2, x3)
new_lt9(x0, x1, ty_Integer)
new_compare114(x0, x1, True)
new_ltEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_lt21(x0, x1, ty_Integer)
new_compare0([], [], x0)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_ltEs10(x0, x1, ty_Float)
new_esEs8(LT, LT)
new_ltEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs23(x0, x1, ty_Double)
new_ltEs7(True, True)
new_esEs7(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_ltEs8(x0, x1)
new_esEs29(x0, x1, app(app(ty_Either, x2), x3))
new_compare27(x0, x1, True, x2, x3, x4)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_lt21(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs18(Left(x0), Left(x1), ty_Bool, x2)
new_lt9(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_lt9(x0, x1, app(app(ty_Either, x2), x3))
new_lt20(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_lt8(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Ordering)
new_esEs28(x0, x1, ty_Ordering)
new_esEs29(x0, x1, ty_@0)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_ltEs11(LT, GT)
new_ltEs11(GT, LT)
new_esEs24(x0, x1, ty_Ordering)
new_lt8(x0, x1, ty_Float)
new_ltEs7(True, False)
new_ltEs7(False, True)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_lt10(x0, x1)
new_esEs7(Right(x0), Right(x1), x2, ty_Integer)
new_esEs23(x0, x1, ty_Int)
new_esEs14(True, True)
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_compare26(x0, x1, True)
new_ltEs19(x0, x1, ty_Integer)
new_compare9(x0, x1, ty_Bool)
new_compare29(x0, x1, True, x2, x3)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Zero)
new_ltEs18(Left(x0), Left(x1), ty_Char, x2)
new_esEs7(Left(x0), Left(x1), ty_Integer, x2)
new_esEs19(x0, x1, ty_Double)
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_compare29(@2(x0, x1), @2(x2, x3), False, x4, x5)
new_lt21(x0, x1, ty_Int)
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_esEs6(Nothing, Nothing, x0)
new_lt6(x0, x1)
new_esEs17(:(x0, x1), [], x2)
new_primMulNat0(Succ(x0), Zero)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs20(x0, x1, ty_Bool)
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Double)
new_esEs7(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs25(x0, x1, ty_Int)
new_compare8(x0, x1, x2)
new_primMulInt(Pos(x0), Pos(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs7(Right(x0), Right(x1), x2, ty_Bool)
new_ltEs18(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs7(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_ltEs18(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_ltEs18(Right(x0), Right(x1), x2, app(ty_[], x3))
new_ltEs19(x0, x1, app(ty_[], x2))
new_esEs29(x0, x1, ty_Bool)
new_esEs7(Left(x0), Left(x1), app(ty_[], x2), x3)
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs29(x0, x1, ty_Ordering)
new_esEs7(Right(x0), Right(x1), x2, ty_Float)
new_ltEs16(x0, x1, x2)
new_ltEs20(x0, x1, ty_Ordering)
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_ltEs10(x0, x1, ty_Char)
new_primEqNat0(Succ(x0), Succ(x1))
new_ltEs18(Right(x0), Right(x1), x2, ty_Int)
new_sr(Integer(x0), Integer(x1))
new_compare9(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs7(Right(x0), Right(x1), x2, ty_Double)
new_esEs7(Left(x0), Left(x1), ty_Int, x2)
new_ltEs18(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs21(x0, x1, ty_Char)
new_lt20(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_lt17(x0, x1, x2)
new_ltEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_ltEs18(Right(x0), Right(x1), x2, ty_Bool)
new_compare16(:%(x0, x1), :%(x2, x3), ty_Integer)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs29(x0, x1, app(ty_[], x2))
new_ltEs10(x0, x1, app(ty_Ratio, x2))
new_ltEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_lt8(x0, x1, ty_@0)
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Bool)
new_esEs7(Left(x0), Left(x1), ty_Double, x2)
new_compare0([], :(x0, x1), x2)
new_compare24(x0, x1, False, x2)
new_lt15(x0, x1)
new_esEs7(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare9(x0, x1, app(ty_[], x2))
new_esEs7(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_lt8(x0, x1, app(ty_[], x2))
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_lt8(x0, x1, ty_Ordering)
new_compare18(Float(x0, x1), Float(x2, x3))
new_esEs20(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Ordering)
new_lt9(x0, x1, ty_Bool)
new_lt8(x0, x1, ty_Integer)
new_lt8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(x0, x1, ty_Bool)
new_compare9(x0, x1, ty_Integer)
new_ltEs19(x0, x1, ty_Double)
new_esEs18(x0, x1, ty_Double)
new_compare26(x0, x1, False)
new_ltEs18(Right(x0), Right(x1), x2, ty_Float)
new_esEs7(Left(x0), Left(x1), ty_@0, x2)
new_compare9(x0, x1, ty_Int)
new_esEs7(Left(x0), Right(x1), x2, x3)
new_esEs7(Right(x0), Left(x1), x2, x3)
new_lt9(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primCompAux0(x0, x1, x2, x3)
new_compare113(x0, x1, x2, x3, False, x4, x5, x6)
new_ltEs18(Left(x0), Left(x1), ty_Double, x2)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_compare28(x0, x1, True, x2, x3)
new_primMulNat0(Succ(x0), Succ(x1))
new_ltEs18(Right(x0), Right(x1), x2, ty_Char)
new_lt16(x0, x1, x2)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs20(x0, x1, ty_Float)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs6(Nothing, Just(x0), x1)
new_lt8(x0, x1, app(ty_Maybe, x2))
new_ltEs10(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_ltEs18(Right(x0), Right(x1), x2, ty_@0)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_ltEs19(x0, x1, ty_Ordering)
new_ltEs10(x0, x1, ty_Int)
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Double(x0, x1), Double(x2, x3))
new_compare11(x0, x1, True, x2, x3, x4)
new_compare110(x0, x1, False)
new_esEs23(x0, x1, ty_@0)
new_lt21(x0, x1, app(ty_Maybe, x2))
new_ltEs5(x0, x1)
new_ltEs18(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_compare15(x0, x1, x2, x3, x4)
new_compare9(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_compare9(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs28(x0, x1, ty_Float)
new_compare210(x0, x1, False)
new_esEs29(x0, x1, ty_Float)
new_ltEs18(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_@0)
new_ltEs10(x0, x1, app(ty_[], x2))
new_compare16(:%(x0, x1), :%(x2, x3), ty_Int)
new_compare9(x0, x1, app(ty_Ratio, x2))
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_esEs7(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs7(Left(x0), Left(x1), ty_Char, x2)
new_ltEs20(x0, x1, ty_Double)
new_lt8(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs18(Right(x0), Right(x1), x2, ty_Integer)
new_compare111(x0, x1, x2, x3, True, x4, x5)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs9(x0, x1)
new_esEs29(x0, x1, app(ty_Maybe, x2))
new_compare7(Double(x0, x1), Double(x2, x3))
new_esEs19(x0, x1, ty_@0)
new_lt9(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_lt21(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, ty_Int)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_pePe(True, x0)
new_esEs29(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs20(x0, x1, ty_Integer)
new_esEs8(EQ, EQ)
new_primCmpNat0(Zero, Succ(x0))
new_compare112(x0, x1, True, x2, x3)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(ty_[], x2))
new_ltEs18(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_compare6(Integer(x0), Integer(x1))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs19(x0, x1, ty_Int)
new_esEs7(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs14(False, True)
new_esEs14(True, False)
new_esEs6(Nothing, Just(x0), x1)
new_lt8(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Double)
new_esEs22(x0, x1, app(ty_[], x2))
new_lt12(x0, x1, x2, x3)
new_compare10(x0, x1, True, x2)
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_asAs(True, x0)
new_compare25(x0, x1, x2, x3)
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Double)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_compare10(x0, x1, False, x2)
new_ltEs18(Left(x0), Left(x1), ty_Integer, x2)
new_esEs12(Integer(x0), Integer(x1))
new_primCmpNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Nothing, x1)
new_ltEs13(x0, x1, x2)
new_ltEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Char)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_lt20(x0, x1, ty_Ordering)
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_lt14(x0, x1)
new_esEs24(x0, x1, ty_Float)
new_ltEs10(x0, x1, ty_Integer)
new_ltEs14(x0, x1)
new_primPlusNat1(Zero, Succ(x0))
new_ltEs11(LT, LT)
new_compare24(x0, x1, True, x2)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_ltEs18(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_ltEs18(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_lt20(x0, x1, ty_Integer)
new_ltEs11(EQ, LT)
new_ltEs10(x0, x1, app(ty_Maybe, x2))
new_ltEs11(LT, EQ)
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs29(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Float)
new_lt21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, ty_@0)
new_esEs7(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_compare9(x0, x1, ty_@0)
new_lt9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_ltEs10(x0, x1, app(app(ty_@2, x2), x3))
new_lt9(x0, x1, app(ty_Maybe, x2))
new_primCmpNat0(Zero, Zero)
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_compare28(x0, x1, False, x2, x3)
new_lt8(x0, x1, app(ty_Ratio, x2))
new_compare12(x0, x1)
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_ltEs19(x0, x1, ty_Int)
new_primCompAux00(x0, LT)
new_ltEs18(Left(x0), Left(x1), ty_Float, x2)
new_lt21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_@0)
new_esEs15(@0, @0)
new_esEs27(x0, x1, ty_Bool)
new_compare210(x0, x1, True)
new_esEs19(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Bool)
new_compare9(x0, x1, ty_Double)
new_ltEs15(x0, x1)
new_compare17(Char(x0), Char(x1))
new_esEs19(x0, x1, ty_Ordering)
new_ltEs20(x0, x1, ty_Int)
new_esEs7(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_lt9(x0, x1, app(ty_Ratio, x2))
new_esEs18(x0, x1, ty_Int)
new_esEs28(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs18(Right(x0), Right(x1), x2, ty_Double)
new_esEs29(x0, x1, ty_Integer)
new_esEs7(Right(x0), Right(x1), x2, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_ltEs18(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare114(x0, x1, False)
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Bool)
new_lt4(x0, x1)
new_esEs20(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Int)
new_primCompAux00(x0, GT)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_ltEs18(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_not(True)
new_lt7(x0, x1)
new_esEs18(x0, x1, ty_@0)
new_lt9(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_compare112(x0, x1, False, x2, x3)
new_esEs21(x0, x1, ty_Integer)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_not(False)
new_primCmpNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_compare5(x0, x1)
new_esEs22(x0, x1, ty_Float)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Char)
new_compare0(:(x0, x1), [], x2)
new_esEs7(Left(x0), Left(x1), ty_Ordering, x2)
new_lt8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_compare19(@0, @0)
new_esEs19(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Double)
new_ltEs17(x0, x1)
new_lt9(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs10(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Integer)
new_esEs28(x0, x1, ty_Char)
new_ltEs19(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_Char)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_esEs17([], [], x0)
new_esEs20(x0, x1, ty_Double)
new_esEs29(x0, x1, ty_Char)
new_primPlusNat0(Succ(x0), x1)
new_esEs7(Right(x0), Right(x1), x2, app(ty_[], x3))
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_lt20(x0, x1, app(ty_Maybe, x2))
new_compare111(x0, x1, x2, x3, False, x4, x5)
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs23(x0, x1, ty_Char)
new_compare9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_lt21(x0, x1, ty_Char)
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_primMulInt(Neg(x0), Pos(x1))
new_primMulInt(Pos(x0), Neg(x1))
new_esEs29(x0, x1, ty_Double)
new_compare113(x0, x1, x2, x3, True, x4, x5, x6)
new_lt9(x0, x1, ty_Ordering)
new_lt21(x0, x1, app(ty_Ratio, x2))
new_ltEs10(x0, x1, ty_Ordering)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_@0)
new_esEs14(False, False)
new_lt5(x0, x1, x2)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs28(x0, x1, ty_Int)
new_ltEs10(x0, x1, ty_Bool)
new_compare14(x0, x1, x2, x3)
new_ltEs20(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs28(x0, x1, ty_Double)
new_esEs18(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_[], x2))
new_ltEs19(x0, x1, ty_Char)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_compare9(x0, x1, app(app(ty_Either, x2), x3))
new_lt21(x0, x1, ty_Bool)
new_esEs18(x0, x1, ty_Integer)
new_pePe(False, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_lt21(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primMulInt(Neg(x0), Neg(x1))
new_lt8(x0, x1, ty_Bool)
new_lt11(x0, x1)
new_esEs22(x0, x1, ty_Ordering)
new_ltEs18(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs19(x0, x1, ty_Float)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_ltEs6(Nothing, Nothing, x0)
new_esEs19(x0, x1, ty_Integer)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Bool)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_compare9(x0, x1, ty_Float)
new_lt21(x0, x1, ty_Float)
new_primPlusNat0(Zero, x0)
new_ltEs7(False, False)
new_lt9(x0, x1, ty_Float)
new_ltEs11(GT, GT)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_lt20(x0, x1, app(app(ty_Either, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookupFM2(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, True, h, ba, bb) → new_lookupFM(vyw19, @2(vyw21, vyw22), h, ba, bb)
new_lookupFM1(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, True, h, ba, bb) → new_lookupFM(vyw20, @2(vyw21, vyw22), h, ba, bb)
new_lookupFM(Branch(@2(vyw300, vyw301), vyw31, vyw32, vyw33, vyw34), @2(vyw40, vyw41), bc, bd, be) → new_lookupFM2(vyw300, vyw301, vyw31, vyw32, vyw33, vyw34, vyw40, vyw41, new_esEs30(vyw40, vyw41, vyw300, vyw301, new_esEs31(vyw40, vyw300, bd), bd, be), bc, bd, be)
new_lookupFM2(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, False, h, ba, bb) → new_lookupFM1(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, new_esEs8(new_compare29(@2(vyw21, vyw22), @2(vyw15, vyw16), new_esEs4(@2(vyw21, vyw22), @2(vyw15, vyw16), ba, bb), ba, bb), GT), h, ba, bb)

The TRS R consists of the following rules:

new_esEs23(vyw401, vyw3001, app(app(ty_Either, cac), cad)) → new_esEs7(vyw401, vyw3001, cac, cad)
new_lt4(vyw430, vyw450) → new_esEs8(new_compare5(vyw430, vyw450), LT)
new_compare17(Char(vyw4300), Char(vyw4500)) → new_primCmpNat0(vyw4300, vyw4500)
new_esEs7(Left(vyw400), Left(vyw3000), app(app(ty_Either, cdc), cdd), gh) → new_esEs7(vyw400, vyw3000, cdc, cdd)
new_lt8(vyw4311, vyw4511, app(ty_Maybe, bcd)) → new_lt17(vyw4311, vyw4511, bcd)
new_esEs25(vyw401, vyw3001, ty_Integer) → new_esEs12(vyw401, vyw3001)
new_ltEs10(vyw4312, vyw4512, app(ty_Maybe, bbb)) → new_ltEs6(vyw4312, vyw4512, bbb)
new_ltEs11(LT, GT) → True
new_esEs24(vyw400, vyw3000, app(app(app(ty_@3, cbg), cbh), cca)) → new_esEs5(vyw400, vyw3000, cbg, cbh, cca)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Char) → new_ltEs14(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, app(app(ty_Either, cce), ccf)) → new_lt19(vyw430, vyw450, cce, ccf)
new_compare7(Double(vyw4300, vyw4301), Double(vyw4500, vyw4501)) → new_compare5(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_esEs31(vyw40, vyw300, ty_Ordering) → new_esEs8(vyw40, vyw300)
new_esEs7(Right(vyw400), Right(vyw3000), gg, app(ty_[], cfd)) → new_esEs17(vyw400, vyw3000, cfd)
new_esEs23(vyw401, vyw3001, app(app(ty_@2, cah), cba)) → new_esEs4(vyw401, vyw3001, cah, cba)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Int, gh) → new_esEs9(vyw400, vyw3000)
new_esEs18(vyw401, vyw3001, app(ty_[], bfb)) → new_esEs17(vyw401, vyw3001, bfb)
new_esEs23(vyw401, vyw3001, ty_Bool) → new_esEs14(vyw401, vyw3001)
new_lt21(vyw4310, vyw4510, ty_@0) → new_lt18(vyw4310, vyw4510)
new_ltEs6(Nothing, Just(vyw4510), cfe) → True
new_esEs29(vyw4310, vyw4510, ty_Int) → new_esEs9(vyw4310, vyw4510)
new_esEs20(vyw4311, vyw4511, ty_Int) → new_esEs9(vyw4311, vyw4511)
new_esEs31(vyw40, vyw300, app(app(app(ty_@3, ha), hb), hc)) → new_esEs5(vyw40, vyw300, ha, hb, hc)
new_esEs23(vyw401, vyw3001, app(ty_[], cbb)) → new_esEs17(vyw401, vyw3001, cbb)
new_lt21(vyw4310, vyw4510, ty_Ordering) → new_lt10(vyw4310, vyw4510)
new_ltEs8(vyw431, vyw451) → new_not(new_esEs8(new_compare5(vyw431, vyw451), GT))
new_lt20(vyw430, vyw450, ty_@0) → new_lt18(vyw430, vyw450)
new_primMulNat0(Zero, Zero) → Zero
new_esEs7(Left(vyw400), Left(vyw3000), app(app(app(ty_@3, cde), cdf), cdg), gh) → new_esEs5(vyw400, vyw3000, cde, cdf, cdg)
new_lt9(vyw4310, vyw4510, ty_Ordering) → new_lt10(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Double) → new_esEs16(vyw400, vyw3000)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(app(ty_@2, chh), daa), chg) → new_ltEs12(vyw4310, vyw4510, chh, daa)
new_esEs28(vyw400, vyw3000, app(ty_Ratio, dcd)) → new_esEs10(vyw400, vyw3000, dcd)
new_sr(Integer(vyw43000), Integer(vyw45010)) → Integer(new_primMulInt(vyw43000, vyw45010))
new_esEs32(vyw32, vyw34, ty_@0) → new_esEs15(vyw32, vyw34)
new_lt21(vyw4310, vyw4510, ty_Float) → new_lt15(vyw4310, vyw4510)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Bool, gh) → new_esEs14(vyw400, vyw3000)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_esEs27(vyw430, vyw450, ty_Integer) → new_esEs12(vyw430, vyw450)
new_lt8(vyw4311, vyw4511, ty_@0) → new_lt18(vyw4311, vyw4511)
new_ltEs10(vyw4312, vyw4512, ty_@0) → new_ltEs17(vyw4312, vyw4512)
new_ltEs20(vyw4311, vyw4511, ty_Char) → new_ltEs14(vyw4311, vyw4511)
new_lt9(vyw4310, vyw4510, ty_Double) → new_lt6(vyw4310, vyw4510)
new_ltEs7(True, True) → True
new_compare9(vyw4300, vyw4500, ty_Integer) → new_compare6(vyw4300, vyw4500)
new_lt21(vyw4310, vyw4510, ty_Char) → new_lt14(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(ty_[], dff)) → new_lt16(vyw4310, vyw4510, dff)
new_lt21(vyw4310, vyw4510, ty_Bool) → new_lt11(vyw4310, vyw4510)
new_esEs30(vyw31, vyw32, vyw33, vyw34, False, bf, bg) → new_esEs8(new_compare29(@2(vyw31, vyw32), @2(vyw33, vyw34), False, bf, bg), LT)
new_esEs10(:%(vyw400, vyw401), :%(vyw3000, vyw3001), gf) → new_asAs(new_esEs26(vyw400, vyw3000, gf), new_esEs25(vyw401, vyw3001, gf))
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Bool) → new_ltEs7(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Right(vyw3000), gg, app(app(app(ty_@3, ceg), ceh), cfa)) → new_esEs5(vyw400, vyw3000, ceg, ceh, cfa)
new_esEs19(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_ltEs20(vyw4311, vyw4511, app(app(ty_@2, ddf), ddg)) → new_ltEs12(vyw4311, vyw4511, ddf, ddg)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(app(ty_Either, dah), dba), chg) → new_ltEs18(vyw4310, vyw4510, dah, dba)
new_compare0(:(vyw4300, vyw4301), :(vyw4500, vyw4501), fb) → new_primCompAux0(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, fb), fb)
new_esEs32(vyw32, vyw34, app(app(ty_@2, cg), da)) → new_esEs4(vyw32, vyw34, cg, da)
new_lt9(vyw4310, vyw4510, app(ty_Maybe, bdf)) → new_lt17(vyw4310, vyw4510, bdf)
new_esEs22(vyw402, vyw3002, app(ty_Maybe, bgh)) → new_esEs6(vyw402, vyw3002, bgh)
new_esEs27(vyw430, vyw450, app(ty_Maybe, dc)) → new_esEs6(vyw430, vyw450, dc)
new_esEs29(vyw4310, vyw4510, ty_Char) → new_esEs11(vyw4310, vyw4510)
new_compare27(vyw430, vyw450, False, dd, de, df) → new_compare11(vyw430, vyw450, new_ltEs9(vyw430, vyw450, dd, de, df), dd, de, df)
new_ltEs18(Right(vyw4310), Left(vyw4510), chf, chg) → False
new_esEs23(vyw401, vyw3001, ty_Integer) → new_esEs12(vyw401, vyw3001)
new_esEs12(Integer(vyw400), Integer(vyw3000)) → new_primEqInt(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, app(app(app(ty_@3, bfg), bfh), bga)) → new_esEs5(vyw400, vyw3000, bfg, bfh, bga)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(app(app(ty_@3, dab), dac), dad), chg) → new_ltEs9(vyw4310, vyw4510, dab, dac, dad)
new_esEs28(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs28(vyw400, vyw3000, app(app(app(ty_@3, dch), dda), ddb)) → new_esEs5(vyw400, vyw3000, dch, dda, ddb)
new_esEs22(vyw402, vyw3002, app(app(ty_Either, bha), bhb)) → new_esEs7(vyw402, vyw3002, bha, bhb)
new_lt9(vyw4310, vyw4510, ty_@0) → new_lt18(vyw4310, vyw4510)
new_compare210(vyw430, vyw450, False) → new_compare114(vyw430, vyw450, new_ltEs11(vyw430, vyw450))
new_lt21(vyw4310, vyw4510, app(app(ty_@2, deh), dfa)) → new_lt12(vyw4310, vyw4510, deh, dfa)
new_esEs7(Right(vyw400), Right(vyw3000), gg, app(ty_Maybe, ced)) → new_esEs6(vyw400, vyw3000, ced)
new_esEs13(Float(vyw400, vyw401), Float(vyw3000, vyw3001)) → new_esEs9(new_sr0(vyw400, vyw3000), new_sr0(vyw401, vyw3001))
new_ltEs10(vyw4312, vyw4512, ty_Int) → new_ltEs8(vyw4312, vyw4512)
new_lt9(vyw4310, vyw4510, app(app(ty_Either, bdg), bdh)) → new_lt19(vyw4310, vyw4510, bdg, bdh)
new_ltEs7(True, False) → False
new_pePe(False, vyw106) → vyw106
new_compare114(vyw430, vyw450, False) → GT
new_esEs29(vyw4310, vyw4510, ty_Double) → new_esEs16(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Left(vyw3000), gg, gh) → False
new_esEs7(Left(vyw400), Right(vyw3000), gg, gh) → False
new_lt20(vyw430, vyw450, ty_Bool) → new_lt11(vyw430, vyw450)
new_ltEs7(False, True) → True
new_esEs19(vyw400, vyw3000, ty_@0) → new_esEs15(vyw400, vyw3000)
new_compare9(vyw4300, vyw4500, ty_Double) → new_compare7(vyw4300, vyw4500)
new_esEs20(vyw4311, vyw4511, ty_Double) → new_esEs16(vyw4311, vyw4511)
new_esEs27(vyw430, vyw450, app(app(ty_Either, cce), ccf)) → new_esEs7(vyw430, vyw450, cce, ccf)
new_esEs19(vyw400, vyw3000, app(ty_Maybe, bfd)) → new_esEs6(vyw400, vyw3000, bfd)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(app(ty_@3, cfh), cga), cgb)) → new_ltEs9(vyw4310, vyw4510, cfh, cga, cgb)
new_esEs22(vyw402, vyw3002, ty_@0) → new_esEs15(vyw402, vyw3002)
new_esEs22(vyw402, vyw3002, app(app(ty_@2, bhf), bhg)) → new_esEs4(vyw402, vyw3002, bhf, bhg)
new_esEs22(vyw402, vyw3002, ty_Integer) → new_esEs12(vyw402, vyw3002)
new_lt20(vyw430, vyw450, app(app(app(ty_@3, dd), de), df)) → new_lt13(vyw430, vyw450, dd, de, df)
new_esEs28(vyw400, vyw3000, ty_@0) → new_esEs15(vyw400, vyw3000)
new_ltEs20(vyw4311, vyw4511, ty_Double) → new_ltEs5(vyw4311, vyw4511)
new_compare11(vyw430, vyw450, False, dd, de, df) → GT
new_esEs27(vyw430, vyw450, app(ty_[], fb)) → new_esEs17(vyw430, vyw450, fb)
new_esEs22(vyw402, vyw3002, ty_Ordering) → new_esEs8(vyw402, vyw3002)
new_esEs19(vyw400, vyw3000, app(app(ty_Either, bfe), bff)) → new_esEs7(vyw400, vyw3000, bfe, bff)
new_ltEs10(vyw4312, vyw4512, ty_Double) → new_ltEs5(vyw4312, vyw4512)
new_compare10(vyw430, vyw450, True, dc) → LT
new_esEs29(vyw4310, vyw4510, app(app(ty_@2, deh), dfa)) → new_esEs4(vyw4310, vyw4510, deh, dfa)
new_ltEs19(vyw431, vyw451, ty_Int) → new_ltEs8(vyw431, vyw451)
new_esEs6(Just(vyw400), Just(vyw3000), app(app(app(ty_@3, ed), ee), ef)) → new_esEs5(vyw400, vyw3000, ed, ee, ef)
new_primCmpNat0(Zero, Succ(vyw45000)) → LT
new_esEs21(vyw4310, vyw4510, ty_Bool) → new_esEs14(vyw4310, vyw4510)
new_esEs32(vyw32, vyw34, ty_Bool) → new_esEs14(vyw32, vyw34)
new_ltEs19(vyw431, vyw451, ty_Float) → new_ltEs15(vyw431, vyw451)
new_esEs31(vyw40, vyw300, app(app(ty_@2, hd), he)) → new_esEs4(vyw40, vyw300, hd, he)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Bool) → new_ltEs7(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Ratio, cgc)) → new_ltEs13(vyw4310, vyw4510, cgc)
new_esEs8(LT, LT) → True
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, app(app(ty_Either, dcb), dcc)) → new_ltEs18(vyw4310, vyw4510, dcb, dcc)
new_esEs19(vyw400, vyw3000, app(ty_[], bgd)) → new_esEs17(vyw400, vyw3000, bgd)
new_esEs32(vyw32, vyw34, ty_Int) → new_esEs9(vyw32, vyw34)
new_compare25(vyw430, vyw450, cce, ccf) → new_compare28(vyw430, vyw450, new_esEs7(vyw430, vyw450, cce, ccf), cce, ccf)
new_esEs28(vyw400, vyw3000, ty_Double) → new_esEs16(vyw400, vyw3000)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Float, gh) → new_esEs13(vyw400, vyw3000)
new_compare10(vyw430, vyw450, False, dc) → GT
new_esEs24(vyw400, vyw3000, app(app(ty_Either, cbe), cbf)) → new_esEs7(vyw400, vyw3000, cbe, cbf)
new_pePe(True, vyw106) → True
new_compare0([], [], fb) → EQ
new_primEqNat0(Zero, Zero) → True
new_compare26(vyw430, vyw450, True) → EQ
new_esEs29(vyw4310, vyw4510, app(ty_Maybe, dfg)) → new_esEs6(vyw4310, vyw4510, dfg)
new_compare29(vyw43, vyw45, True, cgh, cha) → EQ
new_esEs31(vyw40, vyw300, ty_Integer) → new_esEs12(vyw40, vyw300)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_@0) → new_ltEs17(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Integer) → new_lt7(vyw430, vyw450)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Ordering, gh) → new_esEs8(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, ty_Float) → new_esEs13(vyw400, vyw3000)
new_compare24(vyw430, vyw450, False, dc) → new_compare10(vyw430, vyw450, new_ltEs6(vyw430, vyw450, dc), dc)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_[], cgd)) → new_ltEs16(vyw4310, vyw4510, cgd)
new_compare16(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Integer) → new_compare6(new_sr(vyw4300, vyw4501), new_sr(vyw4500, vyw4301))
new_esEs18(vyw401, vyw3001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs5(vyw401, vyw3001, bee, bef, beg)
new_esEs24(vyw400, vyw3000, ty_Double) → new_esEs16(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Integer) → new_ltEs4(vyw4310, vyw4510)
new_esEs8(GT, GT) → True
new_esEs21(vyw4310, vyw4510, ty_Double) → new_esEs16(vyw4310, vyw4510)
new_primPlusNat0(Succ(vyw790), vyw300000) → Succ(Succ(new_primPlusNat1(vyw790, vyw300000)))
new_ltEs15(vyw431, vyw451) → new_not(new_esEs8(new_compare18(vyw431, vyw451), GT))
new_ltEs10(vyw4312, vyw4512, ty_Integer) → new_ltEs4(vyw4312, vyw4512)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Float) → new_ltEs15(vyw4310, vyw4510)
new_esEs7(Right(vyw400), Right(vyw3000), gg, app(app(ty_Either, cee), cef)) → new_esEs7(vyw400, vyw3000, cee, cef)
new_esEs31(vyw40, vyw300, app(app(ty_Either, gg), gh)) → new_esEs7(vyw40, vyw300, gg, gh)
new_compare9(vyw4300, vyw4500, app(app(app(ty_@3, ff), fg), fh)) → new_compare15(vyw4300, vyw4500, ff, fg, fh)
new_lt15(vyw430, vyw450) → new_esEs8(new_compare18(vyw430, vyw450), LT)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_lt9(vyw4310, vyw4510, ty_Integer) → new_lt7(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_Either, cgf), cgg)) → new_ltEs18(vyw4310, vyw4510, cgf, cgg)
new_lt16(vyw430, vyw450, fb) → new_esEs8(new_compare0(vyw430, vyw450, fb), LT)
new_esEs26(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_@0) → new_esEs15(vyw400, vyw3000)
new_primEqInt(Neg(Succ(vyw4000)), Neg(Succ(vyw30000))) → new_primEqNat0(vyw4000, vyw30000)
new_ltEs5(vyw431, vyw451) → new_not(new_esEs8(new_compare7(vyw431, vyw451), GT))
new_esEs7(Left(vyw400), Left(vyw3000), ty_Char, gh) → new_esEs11(vyw400, vyw3000)
new_compare9(vyw4300, vyw4500, ty_Char) → new_compare17(vyw4300, vyw4500)
new_esEs20(vyw4311, vyw4511, ty_Ordering) → new_esEs8(vyw4311, vyw4511)
new_ltEs19(vyw431, vyw451, ty_Double) → new_ltEs5(vyw431, vyw451)
new_esEs23(vyw401, vyw3001, ty_Ordering) → new_esEs8(vyw401, vyw3001)
new_ltEs19(vyw431, vyw451, app(app(app(ty_@3, hh), baa), bab)) → new_ltEs9(vyw431, vyw451, hh, baa, bab)
new_esEs24(vyw400, vyw3000, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, app(ty_Ratio, dbg)) → new_ltEs13(vyw4310, vyw4510, dbg)
new_ltEs20(vyw4311, vyw4511, app(app(app(ty_@3, ddh), dea), deb)) → new_ltEs9(vyw4311, vyw4511, ddh, dea, deb)
new_primPlusNat1(Succ(vyw7900), Zero) → Succ(vyw7900)
new_primPlusNat1(Zero, Succ(vyw3000000)) → Succ(vyw3000000)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, app(app(ty_@2, dbb), dbc)) → new_ltEs12(vyw4310, vyw4510, dbb, dbc)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Float, chg) → new_ltEs15(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Int) → new_lt4(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, ty_@0) → new_esEs15(vyw4310, vyw4510)
new_esEs7(Left(vyw400), Left(vyw3000), app(ty_[], ceb), gh) → new_esEs17(vyw400, vyw3000, ceb)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Float) → new_esEs13(vyw400, vyw3000)
new_lt9(vyw4310, vyw4510, app(app(ty_@2, bcg), bch)) → new_lt12(vyw4310, vyw4510, bcg, bch)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Double) → new_ltEs5(vyw4310, vyw4510)
new_compare111(vyw88, vyw89, vyw90, vyw91, True, bge, bgf) → LT
new_lt7(vyw430, vyw450) → new_esEs8(new_compare6(vyw430, vyw450), LT)
new_lt17(vyw430, vyw450, dc) → new_esEs8(new_compare8(vyw430, vyw450, dc), LT)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vyw401, vyw3001, ty_Char) → new_esEs11(vyw401, vyw3001)
new_compare11(vyw430, vyw450, True, dd, de, df) → LT
new_ltEs10(vyw4312, vyw4512, ty_Char) → new_ltEs14(vyw4312, vyw4512)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_esEs32(vyw32, vyw34, app(app(app(ty_@3, cd), ce), cf)) → new_esEs5(vyw32, vyw34, cd, ce, cf)
new_esEs20(vyw4311, vyw4511, ty_Float) → new_esEs13(vyw4311, vyw4511)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Float) → new_esEs13(vyw400, vyw3000)
new_esEs19(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_compare8(vyw430, vyw450, dc) → new_compare24(vyw430, vyw450, new_esEs6(vyw430, vyw450, dc), dc)
new_compare112(vyw430, vyw450, False, cce, ccf) → GT
new_ltEs19(vyw431, vyw451, ty_Integer) → new_ltEs4(vyw431, vyw451)
new_primEqInt(Neg(Succ(vyw4000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vyw30000))) → False
new_esEs8(EQ, EQ) → True
new_ltEs18(Left(vyw4310), Right(vyw4510), chf, chg) → True
new_esEs32(vyw32, vyw34, app(ty_Ratio, bh)) → new_esEs10(vyw32, vyw34, bh)
new_esEs22(vyw402, vyw3002, ty_Float) → new_esEs13(vyw402, vyw3002)
new_compare9(vyw4300, vyw4500, ty_Float) → new_compare18(vyw4300, vyw4500)
new_ltEs10(vyw4312, vyw4512, ty_Float) → new_ltEs15(vyw4312, vyw4512)
new_esEs22(vyw402, vyw3002, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs5(vyw402, vyw3002, bhc, bhd, bhe)
new_ltEs10(vyw4312, vyw4512, app(app(app(ty_@3, bae), baf), bag)) → new_ltEs9(vyw4312, vyw4512, bae, baf, bag)
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_lt5(vyw430, vyw450, hg) → new_esEs8(new_compare16(vyw430, vyw450, hg), LT)
new_ltEs20(vyw4311, vyw4511, app(app(ty_Either, def), deg)) → new_ltEs18(vyw4311, vyw4511, def, deg)
new_lt9(vyw4310, vyw4510, ty_Char) → new_lt14(vyw4310, vyw4510)
new_esEs29(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_primCmpNat0(Succ(vyw43000), Succ(vyw45000)) → new_primCmpNat0(vyw43000, vyw45000)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs7(Left(vyw400), Left(vyw3000), ty_@0, gh) → new_esEs15(vyw400, vyw3000)
new_esEs18(vyw401, vyw3001, ty_Char) → new_esEs11(vyw401, vyw3001)
new_esEs6(Nothing, Nothing, dg) → True
new_compare16(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Int) → new_compare5(new_sr0(vyw4300, vyw4501), new_sr0(vyw4500, vyw4301))
new_esEs19(vyw400, vyw3000, ty_Char) → new_esEs11(vyw400, vyw3000)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Integer, chg) → new_ltEs4(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(ty_Ratio, dfe)) → new_lt5(vyw4310, vyw4510, dfe)
new_primEqInt(Pos(Succ(vyw4000)), Pos(Succ(vyw30000))) → new_primEqNat0(vyw4000, vyw30000)
new_ltEs10(vyw4312, vyw4512, app(app(ty_@2, bac), bad)) → new_ltEs12(vyw4312, vyw4512, bac, bad)
new_compare9(vyw4300, vyw4500, app(ty_Maybe, gc)) → new_compare8(vyw4300, vyw4500, gc)
new_esEs21(vyw4310, vyw4510, app(ty_Maybe, bdf)) → new_esEs6(vyw4310, vyw4510, bdf)
new_esEs18(vyw401, vyw3001, ty_@0) → new_esEs15(vyw401, vyw3001)
new_esEs32(vyw32, vyw34, app(app(ty_Either, cb), cc)) → new_esEs7(vyw32, vyw34, cb, cc)
new_lt12(vyw430, vyw450, ccg, cch) → new_esEs8(new_compare14(vyw430, vyw450, ccg, cch), LT)
new_esEs14(True, False) → False
new_esEs14(False, True) → False
new_compare9(vyw4300, vyw4500, app(ty_[], gb)) → new_compare0(vyw4300, vyw4500, gb)
new_esEs25(vyw401, vyw3001, ty_Int) → new_esEs9(vyw401, vyw3001)
new_lt9(vyw4310, vyw4510, app(ty_[], bde)) → new_lt16(vyw4310, vyw4510, bde)
new_compare9(vyw4300, vyw4500, ty_Ordering) → new_compare12(vyw4300, vyw4500)
new_esEs6(Nothing, Just(vyw3000), dg) → False
new_esEs6(Just(vyw400), Nothing, dg) → False
new_primEqNat0(Succ(vyw4000), Succ(vyw30000)) → new_primEqNat0(vyw4000, vyw30000)
new_esEs27(vyw430, vyw450, ty_Ordering) → new_esEs8(vyw430, vyw450)
new_compare9(vyw4300, vyw4500, app(app(ty_@2, fc), fd)) → new_compare14(vyw4300, vyw4500, fc, fd)
new_esEs31(vyw40, vyw300, ty_Int) → new_esEs9(vyw40, vyw300)
new_lt8(vyw4311, vyw4511, ty_Bool) → new_lt11(vyw4311, vyw4511)
new_lt14(vyw430, vyw450) → new_esEs8(new_compare17(vyw430, vyw450), LT)
new_primCompAux00(vyw114, LT) → LT
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Char, chg) → new_ltEs14(vyw4310, vyw4510)
new_ltEs17(vyw431, vyw451) → new_not(new_esEs8(new_compare19(vyw431, vyw451), GT))
new_lt9(vyw4310, vyw4510, app(app(app(ty_@3, bda), bdb), bdc)) → new_lt13(vyw4310, vyw4510, bda, bdb, bdc)
new_primCmpInt(Neg(Succ(vyw43000)), Neg(vyw4500)) → new_primCmpNat0(vyw4500, Succ(vyw43000))
new_esEs22(vyw402, vyw3002, ty_Bool) → new_esEs14(vyw402, vyw3002)
new_esEs4(@2(vyw400, vyw401), @2(vyw3000, vyw3001), hd, he) → new_asAs(new_esEs19(vyw400, vyw3000, hd), new_esEs18(vyw401, vyw3001, he))
new_esEs24(vyw400, vyw3000, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_esEs27(vyw430, vyw450, app(app(app(ty_@3, dd), de), df)) → new_esEs5(vyw430, vyw450, dd, de, df)
new_lt13(vyw430, vyw450, dd, de, df) → new_esEs8(new_compare15(vyw430, vyw450, dd, de, df), LT)
new_esEs28(vyw400, vyw3000, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_lt20(vyw430, vyw450, app(ty_Ratio, hg)) → new_lt5(vyw430, vyw450, hg)
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(vyw30000))) → False
new_primEqInt(Pos(Succ(vyw4000)), Pos(Zero)) → False
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Ordering, chg) → new_ltEs11(vyw4310, vyw4510)
new_ltEs19(vyw431, vyw451, app(ty_Maybe, cfe)) → new_ltEs6(vyw431, vyw451, cfe)
new_compare19(@0, @0) → EQ
new_ltEs6(Just(vyw4310), Nothing, cfe) → False
new_primCmpNat0(Zero, Zero) → EQ
new_ltEs10(vyw4312, vyw4512, app(ty_Ratio, bah)) → new_ltEs13(vyw4312, vyw4512, bah)
new_ltEs11(GT, EQ) → False
new_primCmpNat0(Succ(vyw43000), Zero) → GT
new_lt19(vyw430, vyw450, cce, ccf) → new_esEs8(new_compare25(vyw430, vyw450, cce, ccf), LT)
new_ltEs19(vyw431, vyw451, app(ty_Ratio, chd)) → new_ltEs13(vyw431, vyw451, chd)
new_esEs32(vyw32, vyw34, app(ty_Maybe, ca)) → new_esEs6(vyw32, vyw34, ca)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(ty_Maybe, dag), chg) → new_ltEs6(vyw4310, vyw4510, dag)
new_esEs24(vyw400, vyw3000, ty_@0) → new_esEs15(vyw400, vyw3000)
new_primCmpInt(Neg(Zero), Pos(Succ(vyw45000))) → LT
new_esEs23(vyw401, vyw3001, ty_Float) → new_esEs13(vyw401, vyw3001)
new_compare6(Integer(vyw4300), Integer(vyw4500)) → new_primCmpInt(vyw4300, vyw4500)
new_primPlusNat1(Succ(vyw7900), Succ(vyw3000000)) → Succ(Succ(new_primPlusNat1(vyw7900, vyw3000000)))
new_ltEs19(vyw431, vyw451, app(app(ty_@2, chb), chc)) → new_ltEs12(vyw431, vyw451, chb, chc)
new_esEs31(vyw40, vyw300, app(ty_Ratio, gf)) → new_esEs10(vyw40, vyw300, gf)
new_compare28(vyw430, vyw450, True, cce, ccf) → EQ
new_lt8(vyw4311, vyw4511, ty_Char) → new_lt14(vyw4311, vyw4511)
new_primEqInt(Pos(Succ(vyw4000)), Neg(vyw3000)) → False
new_primEqInt(Neg(Succ(vyw4000)), Pos(vyw3000)) → False
new_ltEs16(vyw431, vyw451, che) → new_not(new_esEs8(new_compare0(vyw431, vyw451, che), GT))
new_esEs24(vyw400, vyw3000, app(app(ty_@2, ccb), ccc)) → new_esEs4(vyw400, vyw3000, ccb, ccc)
new_ltEs20(vyw4311, vyw4511, ty_Integer) → new_ltEs4(vyw4311, vyw4511)
new_esEs18(vyw401, vyw3001, app(app(ty_@2, beh), bfa)) → new_esEs4(vyw401, vyw3001, beh, bfa)
new_esEs28(vyw400, vyw3000, ty_Char) → new_esEs11(vyw400, vyw3000)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Char) → new_esEs11(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Float) → new_ltEs15(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Maybe, cge)) → new_ltEs6(vyw4310, vyw4510, cge)
new_ltEs20(vyw4311, vyw4511, ty_Float) → new_ltEs15(vyw4311, vyw4511)
new_compare13(vyw430, vyw450) → new_compare26(vyw430, vyw450, new_esEs14(vyw430, vyw450))
new_esEs26(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs28(vyw400, vyw3000, app(ty_Maybe, dce)) → new_esEs6(vyw400, vyw3000, dce)
new_ltEs11(GT, LT) → False
new_primEqInt(Pos(Zero), Neg(Succ(vyw30000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vyw30000))) → False
new_primCompAux00(vyw114, EQ) → vyw114
new_esEs21(vyw4310, vyw4510, ty_Char) → new_esEs11(vyw4310, vyw4510)
new_primCmpInt(Pos(Zero), Pos(Succ(vyw45000))) → new_primCmpNat0(Zero, Succ(vyw45000))
new_compare15(vyw430, vyw450, dd, de, df) → new_compare27(vyw430, vyw450, new_esEs5(vyw430, vyw450, dd, de, df), dd, de, df)
new_esEs28(vyw400, vyw3000, app(app(ty_Either, dcf), dcg)) → new_esEs7(vyw400, vyw3000, dcf, dcg)
new_esEs23(vyw401, vyw3001, app(ty_Ratio, caa)) → new_esEs10(vyw401, vyw3001, caa)
new_lt8(vyw4311, vyw4511, app(app(ty_Either, bce), bcf)) → new_lt19(vyw4311, vyw4511, bce, bcf)
new_esEs7(Right(vyw400), Right(vyw3000), gg, app(ty_Ratio, cec)) → new_esEs10(vyw400, vyw3000, cec)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, app(app(app(ty_@3, dbd), dbe), dbf)) → new_ltEs9(vyw4310, vyw4510, dbd, dbe, dbf)
new_ltEs11(LT, EQ) → True
new_esEs27(vyw430, vyw450, ty_Double) → new_esEs16(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, app(ty_[], bde)) → new_esEs17(vyw4310, vyw4510, bde)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Int) → new_esEs9(vyw400, vyw3000)
new_ltEs11(LT, LT) → True
new_lt8(vyw4311, vyw4511, app(app(app(ty_@3, bbg), bbh), bca)) → new_lt13(vyw4311, vyw4511, bbg, bbh, bca)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Int, chg) → new_ltEs8(vyw4310, vyw4510)
new_not(False) → True
new_ltEs10(vyw4312, vyw4512, app(ty_[], bba)) → new_ltEs16(vyw4312, vyw4512, bba)
new_primCompAux0(vyw4300, vyw4500, vyw107, fb) → new_primCompAux00(vyw107, new_compare9(vyw4300, vyw4500, fb))
new_compare24(vyw430, vyw450, True, dc) → EQ
new_esEs20(vyw4311, vyw4511, app(ty_Ratio, bcb)) → new_esEs10(vyw4311, vyw4511, bcb)
new_esEs7(Left(vyw400), Left(vyw3000), app(ty_Maybe, cdb), gh) → new_esEs6(vyw400, vyw3000, cdb)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Double, gh) → new_esEs16(vyw400, vyw3000)
new_esEs23(vyw401, vyw3001, ty_@0) → new_esEs15(vyw401, vyw3001)
new_primPlusNat0(Zero, vyw300000) → Succ(vyw300000)
new_primCmpInt(Pos(Succ(vyw43000)), Pos(vyw4500)) → new_primCmpNat0(Succ(vyw43000), vyw4500)
new_esEs29(vyw4310, vyw4510, ty_Integer) → new_esEs12(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(app(ty_Either, dfh), dga)) → new_lt19(vyw4310, vyw4510, dfh, dga)
new_esEs29(vyw4310, vyw4510, app(ty_[], dff)) → new_esEs17(vyw4310, vyw4510, dff)
new_esEs7(Left(vyw400), Left(vyw3000), ty_Integer, gh) → new_esEs12(vyw400, vyw3000)
new_compare113(vyw88, vyw89, vyw90, vyw91, True, vyw93, bge, bgf) → new_compare111(vyw88, vyw89, vyw90, vyw91, True, bge, bgf)
new_esEs32(vyw32, vyw34, ty_Ordering) → new_esEs8(vyw32, vyw34)
new_esEs31(vyw40, vyw300, ty_@0) → new_esEs15(vyw40, vyw300)
new_ltEs12(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), chb, chc) → new_pePe(new_lt21(vyw4310, vyw4510, chb), new_asAs(new_esEs29(vyw4310, vyw4510, chb), new_ltEs20(vyw4311, vyw4511, chc)))
new_ltEs9(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), hh, baa, bab) → new_pePe(new_lt9(vyw4310, vyw4510, hh), new_asAs(new_esEs21(vyw4310, vyw4510, hh), new_pePe(new_lt8(vyw4311, vyw4511, baa), new_asAs(new_esEs20(vyw4311, vyw4511, baa), new_ltEs10(vyw4312, vyw4512, bab)))))
new_lt8(vyw4311, vyw4511, ty_Integer) → new_lt7(vyw4311, vyw4511)
new_esEs24(vyw400, vyw3000, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_lt20(vyw430, vyw450, app(ty_Maybe, dc)) → new_lt17(vyw430, vyw450, dc)
new_esEs7(Left(vyw400), Left(vyw3000), app(ty_Ratio, cda), gh) → new_esEs10(vyw400, vyw3000, cda)
new_compare0(:(vyw4300, vyw4301), [], fb) → GT
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Bool, chg) → new_ltEs7(vyw4310, vyw4510)
new_esEs24(vyw400, vyw3000, app(ty_[], ccd)) → new_esEs17(vyw400, vyw3000, ccd)
new_ltEs11(GT, GT) → True
new_lt20(vyw430, vyw450, ty_Double) → new_lt6(vyw430, vyw450)
new_ltEs10(vyw4312, vyw4512, ty_Ordering) → new_ltEs11(vyw4312, vyw4512)
new_ltEs19(vyw431, vyw451, app(app(ty_Either, chf), chg)) → new_ltEs18(vyw431, vyw451, chf, chg)
new_ltEs20(vyw4311, vyw4511, ty_@0) → new_ltEs17(vyw4311, vyw4511)
new_esEs20(vyw4311, vyw4511, app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs5(vyw4311, vyw4511, bbg, bbh, bca)
new_lt8(vyw4311, vyw4511, ty_Ordering) → new_lt10(vyw4311, vyw4511)
new_primCmpInt(Pos(Succ(vyw43000)), Neg(vyw4500)) → GT
new_esEs22(vyw402, vyw3002, ty_Char) → new_esEs11(vyw402, vyw3002)
new_esEs18(vyw401, vyw3001, app(app(ty_Either, bec), bed)) → new_esEs7(vyw401, vyw3001, bec, bed)
new_esEs27(vyw430, vyw450, ty_@0) → new_esEs15(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, app(app(app(ty_@3, bda), bdb), bdc)) → new_esEs5(vyw4310, vyw4510, bda, bdb, bdc)
new_ltEs19(vyw431, vyw451, app(ty_[], che)) → new_ltEs16(vyw431, vyw451, che)
new_lt18(vyw430, vyw450) → new_esEs8(new_compare19(vyw430, vyw450), LT)
new_primMulInt(Pos(vyw4000), Pos(vyw30000)) → Pos(new_primMulNat0(vyw4000, vyw30000))
new_esEs21(vyw4310, vyw4510, app(app(ty_@2, bcg), bch)) → new_esEs4(vyw4310, vyw4510, bcg, bch)
new_esEs18(vyw401, vyw3001, ty_Float) → new_esEs13(vyw401, vyw3001)
new_esEs18(vyw401, vyw3001, ty_Int) → new_esEs9(vyw401, vyw3001)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, app(ty_[], dbh)) → new_ltEs16(vyw4310, vyw4510, dbh)
new_compare12(vyw430, vyw450) → new_compare210(vyw430, vyw450, new_esEs8(vyw430, vyw450))
new_esEs20(vyw4311, vyw4511, ty_Char) → new_esEs11(vyw4311, vyw4511)
new_primMulInt(Neg(vyw4000), Neg(vyw30000)) → Pos(new_primMulNat0(vyw4000, vyw30000))
new_esEs7(Right(vyw400), Right(vyw3000), gg, app(app(ty_@2, cfb), cfc)) → new_esEs4(vyw400, vyw3000, cfb, cfc)
new_compare110(vyw430, vyw450, True) → LT
new_lt8(vyw4311, vyw4511, app(app(ty_@2, bbe), bbf)) → new_lt12(vyw4311, vyw4511, bbe, bbf)
new_esEs21(vyw4310, vyw4510, app(ty_Ratio, bdd)) → new_esEs10(vyw4310, vyw4510, bdd)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_@0, chg) → new_ltEs17(vyw4310, vyw4510)
new_primEqNat0(Zero, Succ(vyw30000)) → False
new_primEqNat0(Succ(vyw4000), Zero) → False
new_esEs21(vyw4310, vyw4510, ty_Int) → new_esEs9(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, app(app(ty_@2, ccg), cch)) → new_lt12(vyw430, vyw450, ccg, cch)
new_esEs20(vyw4311, vyw4511, ty_Bool) → new_esEs14(vyw4311, vyw4511)
new_compare110(vyw430, vyw450, False) → GT
new_esEs20(vyw4311, vyw4511, ty_@0) → new_esEs15(vyw4311, vyw4511)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_ltEs18(Left(vyw4310), Left(vyw4510), app(ty_[], daf), chg) → new_ltEs16(vyw4310, vyw4510, daf)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_@0) → new_ltEs17(vyw4310, vyw4510)
new_esEs30(vyw31, vyw32, vyw33, vyw34, True, bf, bg) → new_esEs8(new_compare29(@2(vyw31, vyw32), @2(vyw33, vyw34), new_esEs32(vyw32, vyw34, bg), bf, bg), LT)
new_esEs20(vyw4311, vyw4511, app(ty_[], bcc)) → new_esEs17(vyw4311, vyw4511, bcc)
new_esEs22(vyw402, vyw3002, ty_Int) → new_esEs9(vyw402, vyw3002)
new_compare210(vyw430, vyw450, True) → EQ
new_ltEs19(vyw431, vyw451, ty_Ordering) → new_ltEs11(vyw431, vyw451)
new_esEs22(vyw402, vyw3002, app(ty_[], bhh)) → new_esEs17(vyw402, vyw3002, bhh)
new_compare18(Float(vyw4300, vyw4301), Float(vyw4500, vyw4501)) → new_compare5(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_ltEs19(vyw431, vyw451, ty_@0) → new_ltEs17(vyw431, vyw451)
new_lt20(vyw430, vyw450, ty_Char) → new_lt14(vyw430, vyw450)
new_esEs21(vyw4310, vyw4510, app(app(ty_Either, bdg), bdh)) → new_esEs7(vyw4310, vyw4510, bdg, bdh)
new_ltEs20(vyw4311, vyw4511, app(ty_Maybe, dee)) → new_ltEs6(vyw4311, vyw4511, dee)
new_compare9(vyw4300, vyw4500, ty_Bool) → new_compare13(vyw4300, vyw4500)
new_esEs29(vyw4310, vyw4510, app(app(app(ty_@3, dfb), dfc), dfd)) → new_esEs5(vyw4310, vyw4510, dfb, dfc, dfd)
new_ltEs19(vyw431, vyw451, ty_Bool) → new_ltEs7(vyw431, vyw451)
new_esEs27(vyw430, vyw450, app(ty_Ratio, hg)) → new_esEs10(vyw430, vyw450, hg)
new_esEs24(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs18(vyw401, vyw3001, ty_Double) → new_esEs16(vyw401, vyw3001)
new_lt10(vyw430, vyw450) → new_esEs8(new_compare12(vyw430, vyw450), LT)
new_primCmpInt(Neg(Zero), Neg(Succ(vyw45000))) → new_primCmpNat0(Succ(vyw45000), Zero)
new_primCmpInt(Pos(Zero), Neg(Succ(vyw45000))) → GT
new_esEs7(Left(vyw400), Left(vyw3000), app(app(ty_@2, cdh), cea), gh) → new_esEs4(vyw400, vyw3000, cdh, cea)
new_esEs32(vyw32, vyw34, ty_Float) → new_esEs13(vyw32, vyw34)
new_compare5(vyw430, vyw450) → new_primCmpInt(vyw430, vyw450)
new_esEs16(Double(vyw400, vyw401), Double(vyw3000, vyw3001)) → new_esEs9(new_sr0(vyw400, vyw3000), new_sr0(vyw401, vyw3001))
new_esEs29(vyw4310, vyw4510, ty_@0) → new_esEs15(vyw4310, vyw4510)
new_sr0(vyw400, vyw3000) → new_primMulInt(vyw400, vyw3000)
new_esEs27(vyw430, vyw450, ty_Int) → new_esEs9(vyw430, vyw450)
new_ltEs20(vyw4311, vyw4511, ty_Ordering) → new_ltEs11(vyw4311, vyw4511)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Bool) → new_esEs14(vyw400, vyw3000)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Double) → new_esEs16(vyw400, vyw3000)
new_lt8(vyw4311, vyw4511, ty_Int) → new_lt4(vyw4311, vyw4511)
new_ltEs19(vyw431, vyw451, ty_Char) → new_ltEs14(vyw431, vyw451)
new_esEs6(Just(vyw400), Just(vyw3000), app(ty_[], fa)) → new_esEs17(vyw400, vyw3000, fa)
new_esEs18(vyw401, vyw3001, ty_Integer) → new_esEs12(vyw401, vyw3001)
new_esEs11(Char(vyw400), Char(vyw3000)) → new_primEqNat0(vyw400, vyw3000)
new_lt8(vyw4311, vyw4511, ty_Float) → new_lt15(vyw4311, vyw4511)
new_ltEs20(vyw4311, vyw4511, app(ty_[], ded)) → new_ltEs16(vyw4311, vyw4511, ded)
new_esEs20(vyw4311, vyw4511, app(app(ty_Either, bce), bcf)) → new_esEs7(vyw4311, vyw4511, bce, bcf)
new_ltEs11(EQ, EQ) → True
new_lt11(vyw430, vyw450) → new_esEs8(new_compare13(vyw430, vyw450), LT)
new_esEs18(vyw401, vyw3001, app(ty_Maybe, beb)) → new_esEs6(vyw401, vyw3001, beb)
new_lt20(vyw430, vyw450, app(ty_[], fb)) → new_lt16(vyw430, vyw450, fb)
new_ltEs18(Left(vyw4310), Left(vyw4510), ty_Double, chg) → new_ltEs5(vyw4310, vyw4510)
new_lt8(vyw4311, vyw4511, app(ty_Ratio, bcb)) → new_lt5(vyw4311, vyw4511, bcb)
new_ltEs10(vyw4312, vyw4512, app(app(ty_Either, bbc), bbd)) → new_ltEs18(vyw4312, vyw4512, bbc, bbd)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Integer) → new_ltEs4(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, ty_Double) → new_lt6(vyw4310, vyw4510)
new_esEs21(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vyw430, vyw450, ty_Float) → new_esEs13(vyw430, vyw450)
new_lt8(vyw4311, vyw4511, ty_Double) → new_lt6(vyw4311, vyw4511)
new_esEs20(vyw4311, vyw4511, app(ty_Maybe, bcd)) → new_esEs6(vyw4311, vyw4511, bcd)
new_esEs24(vyw400, vyw3000, ty_Char) → new_esEs11(vyw400, vyw3000)
new_ltEs20(vyw4311, vyw4511, ty_Bool) → new_ltEs7(vyw4311, vyw4511)
new_esEs19(vyw400, vyw3000, ty_Double) → new_esEs16(vyw400, vyw3000)
new_esEs15(@0, @0) → True
new_esEs28(vyw400, vyw3000, app(app(ty_@2, ddc), ddd)) → new_esEs4(vyw400, vyw3000, ddc, ddd)
new_asAs(False, vyw60) → False
new_primMulInt(Neg(vyw4000), Pos(vyw30000)) → Neg(new_primMulNat0(vyw4000, vyw30000))
new_primMulInt(Pos(vyw4000), Neg(vyw30000)) → Neg(new_primMulNat0(vyw4000, vyw30000))
new_primMulNat0(Succ(vyw40000), Zero) → Zero
new_primMulNat0(Zero, Succ(vyw300000)) → Zero
new_esEs6(Just(vyw400), Just(vyw3000), app(ty_Maybe, ea)) → new_esEs6(vyw400, vyw3000, ea)
new_esEs21(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_compare29(@2(vyw430, vyw431), @2(vyw450, vyw451), False, cgh, cha) → new_compare113(vyw430, vyw431, vyw450, vyw451, new_lt20(vyw430, vyw450, cgh), new_asAs(new_esEs27(vyw430, vyw450, cgh), new_ltEs19(vyw431, vyw451, cha)), cgh, cha)
new_ltEs11(EQ, LT) → False
new_lt21(vyw4310, vyw4510, app(ty_Maybe, dfg)) → new_lt17(vyw4310, vyw4510, dfg)
new_esEs31(vyw40, vyw300, ty_Double) → new_esEs16(vyw40, vyw300)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Ordering) → new_ltEs11(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, app(app(app(ty_@3, dfb), dfc), dfd)) → new_lt13(vyw4310, vyw4510, dfb, dfc, dfd)
new_esEs23(vyw401, vyw3001, ty_Int) → new_esEs9(vyw401, vyw3001)
new_compare26(vyw430, vyw450, False) → new_compare110(vyw430, vyw450, new_ltEs7(vyw430, vyw450))
new_esEs28(vyw400, vyw3000, ty_Bool) → new_esEs14(vyw400, vyw3000)
new_ltEs18(Left(vyw4310), Left(vyw4510), app(ty_Ratio, dae), chg) → new_ltEs13(vyw4310, vyw4510, dae)
new_esEs6(Just(vyw400), Just(vyw3000), app(app(ty_@2, eg), eh)) → new_esEs4(vyw400, vyw3000, eg, eh)
new_compare14(vyw430, vyw450, ccg, cch) → new_compare29(vyw430, vyw450, new_esEs4(vyw430, vyw450, ccg, cch), ccg, cch)
new_compare28(vyw430, vyw450, False, cce, ccf) → new_compare112(vyw430, vyw450, new_ltEs18(vyw430, vyw450, cce, ccf), cce, ccf)
new_esEs23(vyw401, vyw3001, app(ty_Maybe, cab)) → new_esEs6(vyw401, vyw3001, cab)
new_esEs18(vyw401, vyw3001, ty_Ordering) → new_esEs8(vyw401, vyw3001)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, app(ty_Maybe, dca)) → new_ltEs6(vyw4310, vyw4510, dca)
new_esEs28(vyw400, vyw3000, ty_Float) → new_esEs13(vyw400, vyw3000)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Char) → new_esEs11(vyw400, vyw3000)
new_esEs29(vyw4310, vyw4510, app(ty_Ratio, dfe)) → new_esEs10(vyw4310, vyw4510, dfe)
new_compare111(vyw88, vyw89, vyw90, vyw91, False, bge, bgf) → GT
new_compare9(vyw4300, vyw4500, app(app(ty_Either, gd), ge)) → new_compare25(vyw4300, vyw4500, gd, ge)
new_esEs24(vyw400, vyw3000, app(ty_Ratio, cbc)) → new_esEs10(vyw400, vyw3000, cbc)
new_lt8(vyw4311, vyw4511, app(ty_[], bcc)) → new_lt16(vyw4311, vyw4511, bcc)
new_esEs23(vyw401, vyw3001, ty_Double) → new_esEs16(vyw401, vyw3001)
new_esEs20(vyw4311, vyw4511, app(app(ty_@2, bbe), bbf)) → new_esEs4(vyw4311, vyw4511, bbe, bbf)
new_esEs14(True, True) → True
new_compare113(vyw88, vyw89, vyw90, vyw91, False, vyw93, bge, bgf) → new_compare111(vyw88, vyw89, vyw90, vyw91, vyw93, bge, bgf)
new_esEs27(vyw430, vyw450, ty_Bool) → new_esEs14(vyw430, vyw450)
new_esEs20(vyw4311, vyw4511, ty_Integer) → new_esEs12(vyw4311, vyw4511)
new_esEs32(vyw32, vyw34, app(ty_[], db)) → new_esEs17(vyw32, vyw34, db)
new_esEs5(@3(vyw400, vyw401, vyw402), @3(vyw3000, vyw3001, vyw3002), ha, hb, hc) → new_asAs(new_esEs24(vyw400, vyw3000, ha), new_asAs(new_esEs23(vyw401, vyw3001, hb), new_esEs22(vyw402, vyw3002, hc)))
new_esEs22(vyw402, vyw3002, app(ty_Ratio, bgg)) → new_esEs10(vyw402, vyw3002, bgg)
new_ltEs6(Nothing, Nothing, cfe) → True
new_ltEs4(vyw431, vyw451) → new_not(new_esEs8(new_compare6(vyw431, vyw451), GT))
new_esEs28(vyw400, vyw3000, app(ty_[], dde)) → new_esEs17(vyw400, vyw3000, dde)
new_esEs31(vyw40, vyw300, ty_Char) → new_esEs11(vyw40, vyw300)
new_esEs27(vyw430, vyw450, app(app(ty_@2, ccg), cch)) → new_esEs4(vyw430, vyw450, ccg, cch)
new_esEs7(Right(vyw400), Right(vyw3000), gg, ty_Integer) → new_esEs12(vyw400, vyw3000)
new_esEs6(Just(vyw400), Just(vyw3000), app(ty_Ratio, dh)) → new_esEs10(vyw400, vyw3000, dh)
new_esEs19(vyw400, vyw3000, app(ty_Ratio, bfc)) → new_esEs10(vyw400, vyw3000, bfc)
new_esEs32(vyw32, vyw34, ty_Char) → new_esEs11(vyw32, vyw34)
new_ltEs13(vyw431, vyw451, chd) → new_not(new_esEs8(new_compare16(vyw431, vyw451, chd), GT))
new_esEs31(vyw40, vyw300, ty_Float) → new_esEs13(vyw40, vyw300)
new_esEs6(Just(vyw400), Just(vyw3000), ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_lt21(vyw4310, vyw4510, ty_Int) → new_lt4(vyw4310, vyw4510)
new_lt6(vyw430, vyw450) → new_esEs8(new_compare7(vyw430, vyw450), LT)
new_compare9(vyw4300, vyw4500, app(ty_Ratio, ga)) → new_compare16(vyw4300, vyw4500, ga)
new_ltEs7(False, False) → True
new_ltEs14(vyw431, vyw451) → new_not(new_esEs8(new_compare17(vyw431, vyw451), GT))
new_esEs28(vyw400, vyw3000, ty_Int) → new_esEs9(vyw400, vyw3000)
new_esEs29(vyw4310, vyw4510, app(app(ty_Either, dfh), dga)) → new_esEs7(vyw4310, vyw4510, dfh, dga)
new_esEs14(False, False) → True
new_compare9(vyw4300, vyw4500, ty_Int) → new_compare5(vyw4300, vyw4500)
new_esEs31(vyw40, vyw300, app(ty_[], hf)) → new_esEs17(vyw40, vyw300, hf)
new_esEs22(vyw402, vyw3002, ty_Double) → new_esEs16(vyw402, vyw3002)
new_esEs18(vyw401, vyw3001, ty_Bool) → new_esEs14(vyw401, vyw3001)
new_esEs6(Just(vyw400), Just(vyw3000), ty_@0) → new_esEs15(vyw400, vyw3000)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Ordering) → new_ltEs11(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Ordering) → new_lt10(vyw430, vyw450)
new_primPlusNat1(Zero, Zero) → Zero
new_compare0([], :(vyw4500, vyw4501), fb) → LT
new_lt21(vyw4310, vyw4510, ty_Integer) → new_lt7(vyw4310, vyw4510)
new_lt20(vyw430, vyw450, ty_Float) → new_lt15(vyw430, vyw450)
new_asAs(True, vyw60) → vyw60
new_esEs32(vyw32, vyw34, ty_Integer) → new_esEs12(vyw32, vyw34)
new_compare112(vyw430, vyw450, True, cce, ccf) → LT
new_primMulNat0(Succ(vyw40000), Succ(vyw300000)) → new_primPlusNat0(new_primMulNat0(vyw40000, Succ(vyw300000)), vyw300000)
new_esEs17(:(vyw400, vyw401), :(vyw3000, vyw3001), hf) → new_asAs(new_esEs28(vyw400, vyw3000, hf), new_esEs17(vyw401, vyw3001, hf))
new_esEs6(Just(vyw400), Just(vyw3000), app(app(ty_Either, eb), ec)) → new_esEs7(vyw400, vyw3000, eb, ec)
new_esEs32(vyw32, vyw34, ty_Double) → new_esEs16(vyw32, vyw34)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Char) → new_ltEs14(vyw4310, vyw4510)
new_compare27(vyw430, vyw450, True, dd, de, df) → EQ
new_esEs17([], [], hf) → True
new_esEs24(vyw400, vyw3000, ty_Float) → new_esEs13(vyw400, vyw3000)
new_esEs17(:(vyw400, vyw401), [], hf) → False
new_esEs17([], :(vyw3000, vyw3001), hf) → False
new_lt9(vyw4310, vyw4510, ty_Int) → new_lt4(vyw4310, vyw4510)
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Double) → new_ltEs5(vyw4310, vyw4510)
new_esEs23(vyw401, vyw3001, app(app(app(ty_@3, cae), caf), cag)) → new_esEs5(vyw401, vyw3001, cae, caf, cag)
new_esEs19(vyw400, vyw3000, ty_Ordering) → new_esEs8(vyw400, vyw3000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Int) → new_ltEs8(vyw4310, vyw4510)
new_compare9(vyw4300, vyw4500, ty_@0) → new_compare19(vyw4300, vyw4500)
new_ltEs20(vyw4311, vyw4511, ty_Int) → new_ltEs8(vyw4311, vyw4511)
new_esEs21(vyw4310, vyw4510, ty_Integer) → new_esEs12(vyw4310, vyw4510)
new_lt9(vyw4310, vyw4510, app(ty_Ratio, bdd)) → new_lt5(vyw4310, vyw4510, bdd)
new_esEs9(vyw40, vyw300) → new_primEqInt(vyw40, vyw300)
new_esEs31(vyw40, vyw300, ty_Bool) → new_esEs14(vyw40, vyw300)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_@2, cff), cfg)) → new_ltEs12(vyw4310, vyw4510, cff, cfg)
new_esEs24(vyw400, vyw3000, app(ty_Maybe, cbd)) → new_esEs6(vyw400, vyw3000, cbd)
new_ltEs10(vyw4312, vyw4512, ty_Bool) → new_ltEs7(vyw4312, vyw4512)
new_esEs27(vyw430, vyw450, ty_Char) → new_esEs11(vyw430, vyw450)
new_compare114(vyw430, vyw450, True) → LT
new_esEs29(vyw4310, vyw4510, ty_Bool) → new_esEs14(vyw4310, vyw4510)
new_lt9(vyw4310, vyw4510, ty_Bool) → new_lt11(vyw4310, vyw4510)
new_primCompAux00(vyw114, GT) → GT
new_esEs31(vyw40, vyw300, app(ty_Maybe, dg)) → new_esEs6(vyw40, vyw300, dg)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_lt9(vyw4310, vyw4510, ty_Float) → new_lt15(vyw4310, vyw4510)
new_esEs29(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_esEs19(vyw400, vyw3000, app(app(ty_@2, bgb), bgc)) → new_esEs4(vyw400, vyw3000, bgb, bgc)
new_ltEs11(EQ, GT) → True
new_esEs18(vyw401, vyw3001, app(ty_Ratio, bea)) → new_esEs10(vyw401, vyw3001, bea)
new_ltEs20(vyw4311, vyw4511, app(ty_Ratio, dec)) → new_ltEs13(vyw4311, vyw4511, dec)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_ltEs18(Right(vyw4310), Right(vyw4510), chf, ty_Int) → new_ltEs8(vyw4310, vyw4510)
new_primCmpInt(Neg(Succ(vyw43000)), Pos(vyw4500)) → LT
new_not(True) → False

The set Q consists of the following terms:

new_primCompAux00(x0, EQ)
new_compare110(x0, x1, True)
new_esEs20(x0, x1, ty_Bool)
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(Right(x0), Right(x1), x2, ty_Integer)
new_compare24(x0, x1, False, x2)
new_ltEs20(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_ltEs11(EQ, GT)
new_esEs7(Right(x0), Right(x1), x2, ty_Ordering)
new_ltEs11(GT, EQ)
new_ltEs4(x0, x1)
new_esEs7(Left(x0), Left(x1), ty_Integer, x2)
new_lt8(x0, x1, ty_Int)
new_lt12(x0, x1, x2, x3)
new_lt9(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Integer)
new_ltEs18(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_compare13(x0, x1)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_ltEs10(x0, x1, app(ty_Maybe, x2))
new_esEs7(Left(x0), Left(x1), ty_Double, x2)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Char(x0), Char(x1))
new_ltEs18(Left(x0), Left(x1), ty_Char, x2)
new_ltEs19(x0, x1, ty_Bool)
new_esEs29(x0, x1, ty_Int)
new_ltEs11(EQ, EQ)
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Left(x0), Left(x1), ty_Int, x2)
new_ltEs6(Nothing, Nothing, x0)
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_ltEs16(x0, x1, x2)
new_compare113(x0, x1, x2, x3, True, x4, x5, x6)
new_esEs25(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Integer)
new_ltEs18(Right(x0), Right(x1), x2, ty_Int)
new_lt21(x0, x1, ty_Ordering)
new_esEs13(Float(x0, x1), Float(x2, x3))
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_lt18(x0, x1)
new_esEs32(x0, x1, ty_Int)
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs21(x0, x1, ty_Float)
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr0(x0, x1)
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_esEs22(x0, x1, ty_Char)
new_compare29(@2(x0, x1), @2(x2, x3), False, x4, x5)
new_compare9(x0, x1, app(app(ty_Either, x2), x3))
new_lt9(x0, x1, ty_Char)
new_asAs(False, x0)
new_esEs30(x0, x1, x2, x3, True, x4, x5)
new_lt20(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_ltEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs8(GT, GT)
new_ltEs18(Left(x0), Left(x1), ty_Int, x2)
new_esEs20(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_lt9(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_compare114(x0, x1, True)
new_esEs29(x0, x1, app(ty_[], x2))
new_esEs7(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs29(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt21(x0, x1, ty_Integer)
new_ltEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs8(LT, LT)
new_ltEs10(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Double)
new_ltEs7(True, True)
new_ltEs8(x0, x1)
new_ltEs18(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs7(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_lt8(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Float)
new_lt9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs7(Right(x0), Right(x1), x2, ty_Int)
new_esEs31(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Int)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_lt20(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_lt8(x0, x1, ty_Double)
new_esEs29(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs28(x0, x1, ty_Ordering)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_ltEs11(LT, GT)
new_ltEs11(GT, LT)
new_esEs24(x0, x1, ty_Ordering)
new_lt8(x0, x1, ty_Float)
new_ltEs7(True, False)
new_ltEs7(False, True)
new_lt10(x0, x1)
new_ltEs6(Just(x0), Nothing, x1)
new_esEs23(x0, x1, ty_Int)
new_esEs7(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_compare14(x0, x1, x2, x3)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs14(True, True)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_lt9(x0, x1, app(app(ty_Either, x2), x3))
new_compare26(x0, x1, True)
new_ltEs19(x0, x1, ty_Integer)
new_esEs31(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare9(x0, x1, ty_Bool)
new_compare28(x0, x1, False, x2, x3)
new_esEs31(x0, x1, app(ty_Ratio, x2))
new_compare27(x0, x1, False, x2, x3, x4)
new_primEqNat0(Zero, Zero)
new_lt21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(x0, x1, ty_Double)
new_lt19(x0, x1, x2, x3)
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_lt21(x0, x1, ty_Int)
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_lt6(x0, x1)
new_lt17(x0, x1, x2)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs7(Right(x0), Right(x1), x2, ty_Char)
new_ltEs20(x0, x1, ty_Bool)
new_esEs31(x0, x1, ty_@0)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Double)
new_esEs31(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_primMulInt(Pos(x0), Pos(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs32(x0, x1, ty_Double)
new_esEs17(:(x0, x1), [], x2)
new_compare29(x0, x1, True, x2, x3)
new_esEs29(x0, x1, ty_Bool)
new_esEs32(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Zero)
new_esEs7(Left(x0), Left(x1), ty_@0, x2)
new_esEs29(x0, x1, ty_Ordering)
new_compare24(x0, x1, True, x2)
new_ltEs20(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs10(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_ltEs18(Right(x0), Right(x1), x2, ty_Float)
new_sr(Integer(x0), Integer(x1))
new_ltEs18(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Char)
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Ordering)
new_compare11(x0, x1, False, x2, x3, x4)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs7(Left(x0), Left(x1), ty_Char, x2)
new_compare16(:%(x0, x1), :%(x2, x3), ty_Integer)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare10(x0, x1, False, x2)
new_ltEs18(Left(x0), Left(x1), ty_@0, x2)
new_ltEs20(x0, x1, ty_Integer)
new_esEs29(x0, x1, app(app(ty_Either, x2), x3))
new_esEs32(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_lt8(x0, x1, ty_@0)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt15(x0, x1)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Nothing, x1)
new_ltEs18(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_ltEs18(Right(x0), Right(x1), x2, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_@0)
new_lt8(x0, x1, ty_Ordering)
new_compare18(Float(x0, x1), Float(x2, x3))
new_esEs20(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Ordering)
new_lt9(x0, x1, ty_Bool)
new_lt8(x0, x1, ty_Integer)
new_esEs18(x0, x1, ty_Bool)
new_ltEs18(Right(x0), Right(x1), x2, ty_Bool)
new_compare9(x0, x1, ty_Integer)
new_ltEs19(x0, x1, ty_Double)
new_esEs18(x0, x1, ty_Double)
new_esEs7(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs32(x0, x1, app(ty_Ratio, x2))
new_compare26(x0, x1, False)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_compare9(x0, x1, ty_Int)
new_esEs32(x0, x1, ty_@0)
new_esEs7(Right(x0), Right(x1), x2, ty_Integer)
new_lt9(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_lt5(x0, x1, x2)
new_esEs31(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs7(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs29(x0, x1, app(app(ty_@2, x2), x3))
new_lt20(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_compare9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_ltEs10(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs10(x0, x1, ty_@0)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_esEs29(x0, x1, app(ty_Ratio, x2))
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_ltEs18(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs7(Left(x0), Left(x1), ty_Bool, x2)
new_esEs31(x0, x1, ty_Double)
new_ltEs19(x0, x1, app(ty_[], x2))
new_primCmpInt(Neg(Zero), Neg(Zero))
new_compare111(x0, x1, x2, x3, True, x4, x5)
new_ltEs19(x0, x1, ty_Ordering)
new_esEs16(Double(x0, x1), Double(x2, x3))
new_ltEs10(x0, x1, ty_Int)
new_compare110(x0, x1, False)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_ltEs5(x0, x1)
new_lt20(x0, x1, app(ty_[], x2))
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_ltEs18(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs7(Right(x0), Right(x1), x2, ty_Float)
new_lt9(x0, x1, app(ty_[], x2))
new_compare9(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_compare113(x0, x1, x2, x3, False, x4, x5, x6)
new_esEs27(x0, x1, app(ty_[], x2))
new_compare0(:(x0, x1), [], x2)
new_compare9(x0, x1, app(ty_Maybe, x2))
new_compare9(x0, x1, ty_Char)
new_lt21(x0, x1, app(ty_[], x2))
new_ltEs18(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs28(x0, x1, ty_Float)
new_compare210(x0, x1, False)
new_compare27(x0, x1, True, x2, x3, x4)
new_esEs29(x0, x1, ty_Float)
new_compare8(x0, x1, x2)
new_esEs7(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_@0)
new_compare16(:%(x0, x1), :%(x2, x3), ty_Int)
new_esEs20(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_ltEs20(x0, x1, ty_Double)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs9(x0, x1)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt9(x0, x1, app(app(ty_@2, x2), x3))
new_compare7(Double(x0, x1), Double(x2, x3))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_lt8(x0, x1, app(ty_Maybe, x2))
new_ltEs18(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs19(x0, x1, ty_@0)
new_compare0([], :(x0, x1), x2)
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_lt21(x0, x1, ty_Double)
new_compare112(x0, x1, True, x2, x3)
new_esEs7(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_compare9(x0, x1, app(ty_[], x2))
new_ltEs13(x0, x1, x2)
new_esEs31(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Int)
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_pePe(True, x0)
new_lt9(x0, x1, app(ty_Maybe, x2))
new_esEs32(x0, x1, ty_Ordering)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs20(x0, x1, ty_Integer)
new_esEs8(EQ, EQ)
new_primCmpNat0(Zero, Succ(x0))
new_compare6(Integer(x0), Integer(x1))
new_esEs29(x0, x1, app(ty_Maybe, x2))
new_esEs32(x0, x1, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs19(x0, x1, ty_Int)
new_ltEs20(x0, x1, app(ty_[], x2))
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_lt21(x0, x1, app(ty_Ratio, x2))
new_esEs14(False, True)
new_esEs14(True, False)
new_lt8(x0, x1, ty_Char)
new_esEs17([], :(x0, x1), x2)
new_lt8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Double)
new_esEs6(Nothing, Just(x0), x1)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_asAs(True, x0)
new_esEs31(x0, x1, app(ty_Maybe, x2))
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Double)
new_esEs12(Integer(x0), Integer(x1))
new_primCmpNat0(Succ(x0), Zero)
new_ltEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Char)
new_ltEs18(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_lt20(x0, x1, ty_Ordering)
new_lt14(x0, x1)
new_esEs24(x0, x1, ty_Float)
new_compare11(x0, x1, True, x2, x3, x4)
new_ltEs10(x0, x1, ty_Integer)
new_ltEs14(x0, x1)
new_primPlusNat1(Zero, Succ(x0))
new_ltEs11(LT, LT)
new_compare25(x0, x1, x2, x3)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs7(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_lt20(x0, x1, ty_Integer)
new_esEs7(Right(x0), Right(x1), x2, ty_Bool)
new_ltEs11(EQ, LT)
new_ltEs11(LT, EQ)
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_compare111(x0, x1, x2, x3, False, x4, x5)
new_esEs23(x0, x1, ty_Float)
new_compare15(x0, x1, x2, x3, x4)
new_lt20(x0, x1, ty_@0)
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_compare9(x0, x1, ty_@0)
new_esEs7(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat0(Zero, Zero)
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_ltEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs31(x0, x1, ty_Int)
new_lt13(x0, x1, x2, x3, x4)
new_compare12(x0, x1)
new_esEs7(Right(x0), Right(x1), x2, ty_Double)
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_esEs32(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs19(x0, x1, ty_Int)
new_primCompAux00(x0, LT)
new_esEs24(x0, x1, ty_@0)
new_esEs15(@0, @0)
new_esEs27(x0, x1, ty_Bool)
new_compare210(x0, x1, True)
new_esEs19(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Bool)
new_compare9(x0, x1, ty_Double)
new_ltEs15(x0, x1)
new_esEs7(Right(x0), Right(x1), x2, ty_@0)
new_compare17(Char(x0), Char(x1))
new_esEs19(x0, x1, ty_Ordering)
new_ltEs20(x0, x1, ty_Int)
new_esEs18(x0, x1, ty_Int)
new_esEs28(x0, x1, ty_Integer)
new_esEs31(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Float)
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs32(x0, x1, app(app(ty_Either, x2), x3))
new_esEs32(x0, x1, app(ty_[], x2))
new_ltEs10(x0, x1, app(ty_[], x2))
new_ltEs18(Left(x0), Left(x1), ty_Double, x2)
new_esEs29(x0, x1, ty_Integer)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_compare114(x0, x1, False)
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, ty_@0)
new_lt8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs5(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_lt4(x0, x1)
new_esEs20(x0, x1, ty_Char)
new_primCompAux00(x0, GT)
new_not(True)
new_ltEs18(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_lt7(x0, x1)
new_esEs32(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(x0, x1, ty_@0)
new_lt9(x0, x1, ty_Double)
new_compare9(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs21(x0, x1, ty_Integer)
new_lt8(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_compare112(x0, x1, False, x2, x3)
new_not(False)
new_primCmpNat0(Succ(x0), Succ(x1))
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_esEs7(Left(x0), Right(x1), x2, x3)
new_esEs7(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Int)
new_lt21(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(Left(x0), Left(x1), ty_Float, x2)
new_ltEs18(Right(x0), Right(x1), x2, ty_Double)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs32(x0, x1, ty_Char)
new_compare5(x0, x1)
new_esEs22(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Bool)
new_ltEs10(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs31(x0, x1, ty_Char)
new_compare9(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs6(Nothing, Just(x0), x1)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_compare19(@0, @0)
new_esEs7(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Double)
new_ltEs17(x0, x1)
new_lt9(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_lt16(x0, x1, x2)
new_compare0([], [], x0)
new_ltEs18(Right(x0), Right(x1), x2, ty_Ordering)
new_ltEs18(Left(x0), Left(x1), ty_Bool, x2)
new_ltEs10(x0, x1, ty_Double)
new_ltEs18(Right(x0), Right(x1), x2, ty_Char)
new_esEs22(x0, x1, ty_Integer)
new_esEs28(x0, x1, ty_Char)
new_ltEs19(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_Char)
new_esEs17([], [], x0)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_esEs20(x0, x1, ty_Double)
new_esEs29(x0, x1, ty_Char)
new_ltEs18(Left(x0), Left(x1), ty_Float, x2)
new_primPlusNat0(Succ(x0), x1)
new_ltEs18(Right(x0), Left(x1), x2, x3)
new_ltEs18(Left(x0), Right(x1), x2, x3)
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_ltEs18(Left(x0), Left(x1), app(ty_[], x2), x3)
new_lt21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_primMulInt(Neg(x0), Pos(x1))
new_primMulInt(Pos(x0), Neg(x1))
new_esEs29(x0, x1, ty_Double)
new_lt9(x0, x1, ty_Ordering)
new_esEs30(x0, x1, x2, x3, False, x4, x5)
new_ltEs10(x0, x1, ty_Ordering)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_@0)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs28(x0, x1, ty_Int)
new_esEs31(x0, x1, ty_Float)
new_lt21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs10(x0, x1, ty_Bool)
new_compare10(x0, x1, True, x2)
new_compare0(:(x0, x1), :(x2, x3), x4)
new_ltEs20(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs28(x0, x1, ty_Double)
new_esEs18(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Ordering)
new_ltEs19(x0, x1, ty_Char)
new_lt21(x0, x1, ty_Bool)
new_esEs18(x0, x1, ty_Integer)
new_pePe(False, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs32(x0, x1, ty_Float)
new_lt21(x0, x1, ty_@0)
new_primMulInt(Neg(x0), Neg(x1))
new_lt8(x0, x1, ty_Bool)
new_ltEs18(Right(x0), Right(x1), x2, app(ty_[], x3))
new_lt11(x0, x1)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Float)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_esEs19(x0, x1, ty_Integer)
new_primCompAux0(x0, x1, x2, x3)
new_esEs28(x0, x1, app(ty_[], x2))
new_ltEs18(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_lt8(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Bool)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_esEs31(x0, x1, ty_Bool)
new_lt21(x0, x1, ty_Float)
new_compare9(x0, x1, ty_Float)
new_primPlusNat0(Zero, x0)
new_ltEs7(False, False)
new_lt9(x0, x1, ty_Float)
new_compare28(x0, x1, True, x2, x3)
new_ltEs11(GT, GT)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: